--- a/CookBook/chunks.ML Wed Mar 18 23:52:51 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,167 +0,0 @@
-
-structure Chunks =
-struct
-
-(* rebuilding the output function from ThyOutput in order to *)
-(* enable the options [gray, linenos] *)
-
-val gray = ref false;
-val linenos = ref false
-
-fun output prts =
- prts
- |> (if ! ThyOutput.quotes then map Pretty.quote else I)
- |> (if ! ThyOutput.display then
- map (Output.output o Pretty.string_of o Pretty.indent (! ThyOutput.indent))
- #> space_implode "\\isasep\\isanewline%\n"
- #> (if ! linenos then (enclose "\\begin{linenos}%\n" "%\n\\end{linenos}") else I)
- #> (if ! gray then (enclose "\\begin{graybox}%\n" "%\n\\end{graybox}") else I)
- #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
- else
- map (Output.output o (if ! ThyOutput.break then Pretty.string_of else Pretty.str_of))
- #> space_implode "\\isasep\\isanewline%\n"
- #> enclose "\\isa{" "}");
-
-
-fun boolean "" = true
- | boolean "true" = true
- | boolean "false" = false
- | boolean s = error ("Bad boolean value: " ^ quote s);
-
-val _ = ThyOutput.add_options
- [("gray", Library.setmp gray o boolean),
- ("linenos", Library.setmp linenos o boolean)]
-
-
-
-
-(** theory data **)
-
-structure ChunkData = TheoryDataFun
-(
- type T = (ML_Lex.token list * stamp) NameSpace.table
- val empty = NameSpace.empty_table;
- val copy = I;
- val extend = I;
- fun merge _ tables : T = NameSpace.merge_tables (eq_snd (op =)) tables handle Symtab.DUP dup =>
- error ("Attempt to merge different versions of ML chunk " ^ quote dup);
-);
-
-fun declare_chunk name thy =
- (Sign.full_bname thy name,
- ChunkData.map (snd o NameSpace.define (Sign.naming_of thy)
- (Binding.name name, ([], stamp ()))) thy
- handle Symtab.DUP _ => error ("Duplicate definition of ML chunk " ^ quote name));
-
-fun augment_chunk tok name =
- ChunkData.map (apsnd (Symtab.map_entry name (apfst (cons tok))));
-
-fun the_chunk thy name =
- let val (space, tab) = ChunkData.get thy
- in case Symtab.lookup tab (NameSpace.intern space name) of
- NONE => error ("Unknown ML chunk " ^ quote name)
- | SOME (toks, _) => rev toks
- end;
-
-
-(** parsers **)
-
-val not_eof = ML_Lex.stopper |> Scan.is_stopper #> not;
-
-val scan_space = Scan.many Symbol.is_blank;
-
-fun scan_cmt scan =
- Scan.one (ML_Lex.kind_of #> equal ML_Lex.Comment) >>
- (ML_Lex.content_of #> Symbol.explode #> Scan.finite Symbol.stopper scan #> fst);
-
-val scan_chunks = Scan.depend (fn (open_chunks, thy) =>
- scan_cmt ((Scan.this_string "(*" -- scan_space -- Scan.this_string "@chunk" --
- scan_space) |-- Symbol.scan_id --|
- (scan_space -- Scan.this_string "*)") >> (fn name =>
- let val (name', thy') = declare_chunk name thy
- in ((name' :: open_chunks, thy'), "") end))
- ||
- scan_cmt (Scan.this_string "(*" -- scan_space -- Scan.this_string "@end" --
- scan_space -- Scan.this_string "*)" >> (fn _ =>
- (case open_chunks of
- [] => error "end without matching chunk encountered"
- | _ :: open_chunks' => ((open_chunks', thy), ""))))
- ||
- Scan.one not_eof >> (fn tok =>
- ((open_chunks, fold (augment_chunk tok) open_chunks thy), ML_Lex.content_of tok)));
-
-fun chunks_of s thy =
- let val toks = Source.exhaust (ML_Lex.source (Source.of_string s))
- in case Scan.finite' ML_Lex.stopper (Scan.repeat (Scan.error scan_chunks))
- (([], thy), toks) of
- (toks', (([], thy'), _)) => (implode toks', thy')
- | (_, ((open_chunks, _), _)) =>
- error ("Open chunks at end of text: " ^ commas_quote open_chunks)
- end;
-
-
-(** use command **)
-
-fun load_ml dir raw_path thy =
- (case ThyLoad.check_ml dir raw_path of
- NONE => error ("Could not find ML file " ^ quote (Path.implode raw_path))
- | SOME (path, _) =>
- let val (s, thy') = chunks_of (File.read path) thy
- in
- Context.theory_map (ThyInfo.exec_file false raw_path) thy'
- end);
-
-fun use_chunks path thy =
- load_ml (ThyInfo.master_directory (Context.theory_name thy)) path thy;
-
-val _ =
- OuterSyntax.command "use_chunks" "eval ML text from file"
- (OuterKeyword.tag_ml OuterKeyword.thy_decl)
- (OuterParse.path >> (Toplevel.theory o use_chunks));
-
-
-(** antiquotation **)
-
-val str_of_source = space_implode " " o map OuterLex.unparse o #2 o #1 o Args.dest_src;
-
-val verbatim = space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|";
-
-val transform_cmts =
- Scan.finite ML_Lex.stopper (Scan.repeat
- ( scan_cmt
- (Scan.this_string "(*{" |--
- Scan.repeat (Scan.unless (Scan.this_string "}*)")
- (Scan.one (not o Symbol.is_eof))) --|
- Scan.this_string "}*)" >>
- (Symbol.encode_raw o enclose "\\hfill\\textrm{\\textit{" "}}" o implode))
- || Scan.one not_eof >> ML_Lex.content_of)) #>
- fst;
-
-fun output_chunk {state: Toplevel.state, source = src, context = ctxt} name =
- let
- val toks = the_chunk (ProofContext.theory_of ctxt) name;
- val (spc, toks') = (case toks of
- [] => ("", [])
- | [tok] => ("", [tok])
- | tok :: toks' =>
- let
- val (toks'', tok') = split_last toks'
- val toks''' =
- if ML_Lex.kind_of tok' = ML_Lex.Space then toks''
- else toks'
- in
- if ML_Lex.kind_of tok = ML_Lex.Space then
- (tok |> ML_Lex.content_of |> Symbol.explode |>
- take_suffix (equal " ") |> snd |> implode,
- toks''')
- else ("", tok :: toks''')
- end)
- val txt = spc ^ implode (transform_cmts toks')
- in
- txt |> split_lines |>
- (map Pretty.str) |> output
- end;
-
-val _ = ThyOutput.antiquotation "ML_chunk" (Scan.lift Args.name) output_chunk;
-
-end;