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;