--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/CookBook/chunks.ML	Fri Oct 10 17:04:05 2008 +0200
@@ -0,0 +1,135 @@
+structure Chunks =
+struct
+
+(** 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_name thy name,
+   ChunkData.map (NameSpace.extend_table (Sign.naming_of thy) [(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 "}*)" >>
+           (enclose "\\hfill\\textrm{\\textit{" "}}" o implode))
+     || Scan.one not_eof >> ML_Lex.content_of)) #>
+  fst;
+
+fun output_chunk src 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
+    ((if ! ThyOutput.source then str_of_source src else txt)
+    |> (if ! ThyOutput.quotes then quote else I)
+    |> (if ! ThyOutput.display then enclose "\\begin{alltt}\n" "\n\\end{alltt}"
+        else split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"))
+  end;
+
+val _ = ThyOutput.add_commands
+  [("ML_chunk", ThyOutput.args (Scan.lift Args.name) output_chunk)];
+
+end;