src/Doc/antiquote_setup.ML
changeset 54372 2d61935eed4a
parent 53061 417cb0f713e0
child 54705 0dff3326d12a
equal deleted inserted replaced
54371:52ed202464a5 54372:2d61935eed4a
    43 val verbatim = space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|";
    43 val verbatim = space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|";
    44 
    44 
    45 val verbatim_setup =
    45 val verbatim_setup =
    46   Thy_Output.antiquotation @{binding verbatim} (Scan.lift Args.name)
    46   Thy_Output.antiquotation @{binding verbatim} (Scan.lift Args.name)
    47     (K (split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"));
    47     (K (split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"));
       
    48 
       
    49 
       
    50 (* unchecked file *)
       
    51 
       
    52 val file_unchecked_setup =
       
    53   Thy_Output.antiquotation @{binding file_unchecked} (Scan.lift (Parse.position Parse.path))
       
    54     (fn {context = ctxt, ...} => fn (name, pos) =>
       
    55       let
       
    56         val dir = Thy_Load.master_directory (Proof_Context.theory_of ctxt);
       
    57         val path = Path.append dir (Path.explode name);
       
    58         val _ = Position.report pos (Markup.path name);
       
    59       in
       
    60         space_explode "/" name
       
    61         |> map Thy_Output.verb_text
       
    62         |> space_implode (Thy_Output.verb_text "/" ^ "\\discretionary{}{}{}")
       
    63       end);
    48 
    64 
    49 
    65 
    50 (* ML text *)
    66 (* ML text *)
    51 
    67 
    52 local
    68 local
   231 
   247 
   232 (* theory setup *)
   248 (* theory setup *)
   233 
   249 
   234 val setup =
   250 val setup =
   235   verbatim_setup #>
   251   verbatim_setup #>
       
   252   file_unchecked_setup #>
   236   index_ml_setup #>
   253   index_ml_setup #>
   237   named_thms_setup #>
   254   named_thms_setup #>
   238   thy_file_setup #>
   255   thy_file_setup #>
   239   entity_setup;
   256   entity_setup;
   240 
   257