1 

     2 structure Chunks =

     3 struct

     4 

     5 (* rebuilding the output function from ThyOutput in order to *)

     6 (* enable the options [gray, linenos]                        *)

     7 

     8 val gray = ref false;

     9 val linenos = ref false

    10 

    11 fun output prts =

    12   prts

    13   |> (if ! ThyOutput.quotes then map Pretty.quote else I)

    14   |> (if ! ThyOutput.display then

    15     map (Output.output o Pretty.string_of o Pretty.indent (! ThyOutput.indent))

    16     #> space_implode "\\isasep\\isanewline%\n"

    17     #> (if ! linenos then (enclose "\\begin{linenos}%\n" "%\n\\end{linenos}") else I) 

    18     #> (if ! gray then (enclose "\\begin{graybox}%\n" "%\n\\end{graybox}") else I) 

    19     #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"

    20   else

    21     map (Output.output o (if ! ThyOutput.break then Pretty.string_of else Pretty.str_of))

    22     #> space_implode "\\isasep\\isanewline%\n"

    23     #> enclose "\\isa{" "}");

    24 

    25 

    26 fun boolean "" = true

    27   | boolean "true" = true

    28   | boolean "false" = false

    29   | boolean s = error ("Bad boolean value: " ^ quote s);

    30 

    31 val _ = ThyOutput.add_options

    32  [("gray", Library.setmp gray o boolean),

    33   ("linenos", Library.setmp linenos o boolean)]

    34 

    35 

    36 

    37 

    38 (** theory data **)

    39 

    40 structure ChunkData = TheoryDataFun

    41 (

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

    43   val empty = NameSpace.empty_table;

    44   val copy = I;

    45   val extend = I;

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

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

    48 );

    49 

    50 fun declare_chunk name thy =

    51   (Sign.full_bname thy name,

    52    ChunkData.map (snd o NameSpace.define (Sign.naming_of thy)

    53      (Binding.name name, ([], stamp ()))) thy

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

    55 

    56 fun augment_chunk tok name =

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

    58 

    59 fun the_chunk thy name =

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

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

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

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

    64   end;

    65 

    66 

    67 (** parsers **)

    68 

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

    70 

    71 val scan_space = Scan.many Symbol.is_blank;

    72 

    73 fun scan_cmt scan =

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

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

    76 

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

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

    79     scan_space) |-- Symbol.scan_id --|

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

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

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

    83   ||

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

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

    86       (case open_chunks of

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

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

    89   ||

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

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

    92 

    93 fun chunks_of s thy =

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

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

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

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

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

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

   100   end;

   101 

   102 

   103 (** use command **)

   104 

   105 fun load_ml dir raw_path thy =

   106   (case ThyLoad.check_ml dir raw_path of

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

   108   | SOME (path, _) =>

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

   110       in

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

   112       end);

   113 

   114 fun use_chunks path thy =

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

   116 

   117 val _ =

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

   119     (OuterKeyword.tag_ml OuterKeyword.thy_decl)

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

   121 

   122 

   123 (** antiquotation **)

   124 

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

   126 

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

   128 

   129 val transform_cmts =

   130   Scan.finite ML_Lex.stopper (Scan.repeat

   131     (   scan_cmt

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

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

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

   135            Scan.this_string "}*)" >>

   136            (Symbol.encode_raw o enclose "\\hfill\\textrm{\\textit{" "}}" o implode))

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

   138   fst;

   139 

   140 fun output_chunk {state: Toplevel.state, source = src, context = ctxt} name =

   141   let

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

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

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

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

   146       | tok :: toks' =>

   147           let

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

   149             val toks''' =

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

   151               else toks'

   152           in

   153             if ML_Lex.kind_of tok = ML_Lex.Space then

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

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

   156                toks''')

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

   158           end)

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

   160   in

   161     txt |> split_lines |>

   162     (map Pretty.str) |> output 

   163   end;

   164 

   165 val _ = ThyOutput.antiquotation "ML_chunk" (Scan.lift Args.name) output_chunk;

   166 

   167 end;