1 structure Chunks =

     2 struct

     3 

     4 (** theory data **)

     5 

     6 structure ChunkData = TheoryDataFun

     7 (

     8   type T = (ML_Lex.token list * stamp) NameSpace.table

     9   val empty = NameSpace.empty_table;

    10   val copy = I;

    11   val extend = I;

    12   fun merge _ tables : T = NameSpace.merge_tables (eq_snd (op =)) tables handle Symtab.DUP dup =>

    13     error ("Attempt to merge different versions of ML chunk " ^ quote dup);

    14 );

    15 

    16 fun declare_chunk name thy =

    17   (Sign.full_name thy name,

    18    ChunkData.map (NameSpace.extend_table (Sign.naming_of thy) [(name, ([], stamp ()))]) thy

    19    handle Symtab.DUP _ => error ("Duplicate definition of ML chunk " ^ quote name));

    20 

    21 fun augment_chunk tok name =

    22   ChunkData.map (apsnd (Symtab.map_entry name (apfst (cons tok))));

    23 

    24 fun the_chunk thy name =

    25   let val (space, tab) = ChunkData.get thy

    26   in case Symtab.lookup tab (NameSpace.intern space name) of

    27       NONE => error ("Unknown ML chunk " ^ quote name)

    28     | SOME (toks, _) => rev toks

    29   end;

    30 

    31 

    32 (** parsers **)

    33 

    34 val not_eof = ML_Lex.stopper |> Scan.is_stopper #> not;

    35 

    36 val scan_space = Scan.many Symbol.is_blank;

    37 

    38 fun scan_cmt scan =

    39   Scan.one (ML_Lex.kind_of #> equal ML_Lex.Comment) >>

    40   (ML_Lex.content_of #> Symbol.explode #> Scan.finite Symbol.stopper scan #> fst);

    41 

    42 val scan_chunks = Scan.depend (fn (open_chunks, thy) =>

    43   scan_cmt ((Scan.this_string "(*" -- scan_space -- Scan.this_string "@chunk" --

    44     scan_space) |-- Symbol.scan_id --|

    45     (scan_space -- Scan.this_string "*)") >> (fn name =>

    46       let val (name', thy') = declare_chunk name thy

    47       in ((name' :: open_chunks, thy'), "") end))

    48   ||

    49   scan_cmt (Scan.this_string "(*" -- scan_space -- Scan.this_string "@end" --

    50     scan_space -- Scan.this_string "*)" >> (fn _ =>

    51       (case open_chunks of

    52          [] => error "end without matching chunk encountered"

    53        | _ :: open_chunks' => ((open_chunks', thy), ""))))

    54   ||

    55   Scan.one not_eof >> (fn tok =>

    56     ((open_chunks, fold (augment_chunk tok) open_chunks thy), ML_Lex.content_of tok)));

    57 

    58 fun chunks_of s thy =

    59   let val toks = Source.exhaust (ML_Lex.source (Source.of_string s))

    60   in case Scan.finite' ML_Lex.stopper (Scan.repeat (Scan.error scan_chunks))

    61         (([], thy), toks) of

    62       (toks', (([], thy'), _)) => (implode toks', thy')

    63     | (_, ((open_chunks, _), _)) =>

    64         error ("Open chunks at end of text: " ^ commas_quote open_chunks)

    65   end;

    66 

    67 

    68 (** use command **)

    69 

    70 fun load_ml dir raw_path thy =

    71   (case ThyLoad.check_ml dir raw_path of

    72     NONE => error ("Could not find ML file " ^ quote (Path.implode raw_path))

    73   | SOME (path, _) =>

    74       let val (s, thy') = chunks_of (File.read path) thy

    75       in

    76         Context.theory_map (ThyInfo.exec_file false raw_path) thy'

    77       end);

    78 

    79 fun use_chunks path thy =

    80   load_ml (ThyInfo.master_directory (Context.theory_name thy)) path thy;

    81 

    82 val _ =

    83   OuterSyntax.command "use_chunks" "eval ML text from file"

    84     (OuterKeyword.tag_ml OuterKeyword.thy_decl)

    85     (OuterParse.path >> (Toplevel.theory o use_chunks));

    86 

    87 

    88 (** antiquotation **)

    89 

    90 val str_of_source = space_implode " " o map OuterLex.unparse o #2 o #1 o Args.dest_src;

    91 

    92 val verbatim = space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|";

    93 

    94 val transform_cmts =

    95   Scan.finite ML_Lex.stopper (Scan.repeat

    96     (   scan_cmt

    97           (Scan.this_string "(*{" |--

    98            Scan.repeat (Scan.unless (Scan.this_string "}*)")

    99              (Scan.one (not o Symbol.is_eof))) --|

   100            Scan.this_string "}*)" >>

   101            (enclose "\\hfill\\textrm{\\textit{" "}}" o implode))

   102      || Scan.one not_eof >> ML_Lex.content_of)) #>

   103   fst;

   104 

   105 fun output_chunk src ctxt name =

   106   let

   107     val toks = the_chunk (ProofContext.theory_of ctxt) name;

   108     val (spc, toks') = (case toks of

   109         [] => ("", [])

   110       | [tok] => ("", [tok])

   111       | tok :: toks' =>

   112           let

   113             val (toks'', tok') = split_last toks'

   114             val toks''' =

   115               if ML_Lex.kind_of tok' = ML_Lex.Space then toks''

   116               else toks'

   117           in

   118             if ML_Lex.kind_of tok = ML_Lex.Space then

   119               (tok |> ML_Lex.content_of |> Symbol.explode |>

   120                take_suffix (equal " ") |> snd |> implode,

   121                toks''')

   122             else ("", tok :: toks''')

   123           end)

   124     val txt = spc ^ implode (transform_cmts toks')

   125   in

   126     ((if ! ThyOutput.source then str_of_source src else txt)

   127     |> (if ! ThyOutput.quotes then quote else I)

   128     |> (if ! ThyOutput.display then enclose "\\begin{alltt}\n" "\n\\end{alltt}"

   129         else split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"))

   130   end;

   131 

   132 val _ = ThyOutput.add_commands

   133   [("ML_chunk", ThyOutput.args (Scan.lift Args.name) output_chunk)];

   134 

   135 end;