doem tuning and made the cookbook work again with recent changes (CookBook/Package/Ind_Interface.thy needs to be looked at to see what the problem with the new parser type is)
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_bname thy name, ChunkData.map (snd o NameSpace.bind (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 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 txt |> split_lines |> ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt end;val _ = ThyOutput.add_commands [("ML_chunk", ThyOutput.args (Scan.lift Args.name) output_chunk)];end;