src/Pure/Thy/document_antiquotations.ML
author wenzelm
Wed Dec 09 16:36:26 2015 +0100 (2015-12-09)
changeset 61814 1ca1142e1711
parent 61748 fc53fbf9fe01
child 62058 1cfd5d604937
permissions -rw-r--r--
clarified type Token.src: plain token list, with usual implicit value assignment;
clarified type Token.name_value, notably for head of Token.src;
clarified Attrib/Method check_src vs. parser;
     1 (*  Title:      Pure/ML/document_antiquotations.ML
     2     Author:     Makarius
     3 
     4 Miscellaneous document antiquotations.
     5 *)
     6 
     7 structure Document_Antiquotations: sig end =
     8 struct
     9 
    10 (* control spacing *)
    11 
    12 val _ =
    13   Theory.setup
    14    (Thy_Output.antiquotation @{binding noindent} (Scan.succeed ()) (K (K "\\noindent")) #>
    15     Thy_Output.antiquotation @{binding smallskip} (Scan.succeed ()) (K (K "\\smallskip")) #>
    16     Thy_Output.antiquotation @{binding medskip} (Scan.succeed ()) (K (K "\\medskip")) #>
    17     Thy_Output.antiquotation @{binding bigskip} (Scan.succeed ()) (K (K "\\bigskip")));
    18 
    19 
    20 (* control style *)
    21 
    22 local
    23 
    24 fun control_antiquotation name s1 s2 =
    25   Thy_Output.antiquotation name (Scan.lift Args.cartouche_input)
    26     (fn {state, ...} => enclose s1 s2 o Thy_Output.output_text state {markdown = false});
    27 
    28 in
    29 
    30 val _ =
    31   Theory.setup
    32    (control_antiquotation @{binding footnote} "\\footnote{" "}" #>
    33     control_antiquotation @{binding emph} "\\emph{" "}" #>
    34     control_antiquotation @{binding bold} "\\textbf{" "}");
    35 
    36 end;
    37 
    38 
    39 (* quasi-formal text (unchecked) *)
    40 
    41 local
    42 
    43 fun text_antiquotation name =
    44   Thy_Output.antiquotation name (Scan.lift Args.text_input)
    45     (fn {context = ctxt, ...} => fn source =>
    46      (Context_Position.report ctxt (Input.pos_of source)
    47         (Markup.language_text (Input.is_delimited source));
    48       Thy_Output.output ctxt [Thy_Output.pretty_text ctxt (Input.source_content source)]));
    49 
    50 in
    51 
    52 val _ =
    53   Theory.setup
    54    (text_antiquotation @{binding text} #>
    55     text_antiquotation @{binding cartouche});
    56 
    57 end;
    58 
    59 
    60 (* theory text with tokens (unchecked) *)
    61 
    62 val _ =
    63   Theory.setup
    64     (Thy_Output.antiquotation @{binding theory_text} (Scan.lift Args.text_input)
    65       (fn {context = ctxt, ...} => fn source =>
    66         let
    67           val _ =
    68             Context_Position.report ctxt (Input.pos_of source)
    69               (Markup.language_outer (Input.is_delimited source));
    70 
    71           val keywords = Thy_Header.get_keywords' ctxt;
    72           val toks =
    73             Input.source_explode source
    74             |> not (Config.get ctxt Thy_Output.display) ? Symbol_Pos.trim_lines
    75             |> Source.of_list
    76             |> Token.source' true keywords
    77             |> Source.exhaust;
    78           val _ = Context_Position.reports_text ctxt (maps (Token.reports keywords) toks);
    79           val indentation =
    80             Latex.output_symbols (replicate (Config.get ctxt Thy_Output.indent) Symbol.space);
    81         in
    82           implode (map Latex.output_token toks) |>
    83            (if Config.get ctxt Thy_Output.display then
    84               split_lines #> map (prefix indentation) #> cat_lines #>
    85               Latex.environment "isabelle"
    86             else enclose "\\isa{" "}")
    87         end));
    88 
    89 
    90 (* goal state *)
    91 
    92 local
    93 
    94 fun goal_state name main = Thy_Output.antiquotation name (Scan.succeed ())
    95   (fn {state, context = ctxt, ...} => fn () =>
    96     Thy_Output.output ctxt
    97       [Goal_Display.pretty_goal
    98         (Config.put Goal_Display.show_main_goal main ctxt)
    99         (#goal (Proof.goal (Toplevel.proof_of state)))]);
   100 
   101 in
   102 
   103 val _ = Theory.setup
   104  (goal_state @{binding goals} true #>
   105   goal_state @{binding subgoals} false);
   106 
   107 end;
   108 
   109 
   110 (* embedded lemma *)
   111 
   112 val _ = Theory.setup
   113   (Thy_Output.antiquotation @{binding lemma}
   114     (Scan.lift (Scan.ahead Parse.not_eof) -- Args.prop --
   115       Scan.lift (Parse.position (Parse.reserved "by") -- Method.parse -- Scan.option Method.parse))
   116     (fn {source, context = ctxt, ...} => fn ((prop_token, prop), (((_, by_pos), m1), m2)) =>
   117       let
   118         val reports = (by_pos, Markup.keyword1) :: maps Method.reports_of (m1 :: the_list m2);
   119         val _ = Context_Position.reports ctxt reports;
   120 
   121         (* FIXME check proof!? *)
   122         val _ = ctxt
   123           |> Proof.theorem NONE (K I) [[(prop, [])]]
   124           |> Proof.global_terminal_proof (m1, m2);
   125       in
   126         Thy_Output.output ctxt
   127           (Thy_Output.maybe_pretty_source
   128             Thy_Output.pretty_term ctxt [hd source, prop_token] [prop])
   129       end));
   130 
   131 
   132 (* verbatim text *)
   133 
   134 val _ =
   135   Theory.setup
   136     (Thy_Output.antiquotation @{binding verbatim} (Scan.lift Args.text)
   137       (Thy_Output.verbatim_text o #context));
   138 
   139 
   140 (* ML text *)
   141 
   142 local
   143 
   144 fun ml_text name ml = Thy_Output.antiquotation name (Scan.lift Args.text_input)
   145   (fn {context = ctxt, ...} => fn source =>
   146    (ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (Input.pos_of source) (ml source);
   147     Thy_Output.verbatim_text ctxt (Input.source_content source)));
   148 
   149 fun ml_enclose bg en source =
   150   ML_Lex.read bg @ ML_Lex.read_source false source @ ML_Lex.read en;
   151 
   152 in
   153 
   154 val _ = Theory.setup
   155  (ml_text @{binding ML} (ml_enclose "fn _ => (" ");") #>
   156   ml_text @{binding ML_op} (ml_enclose "fn _ => (op " ");") #>
   157   ml_text @{binding ML_type} (ml_enclose "val _ = NONE : (" ") option;") #>
   158   ml_text @{binding ML_structure}
   159     (ml_enclose "functor XXX() = struct structure XX = " " end;") #>
   160 
   161   ml_text @{binding ML_functor}   (* FIXME formal treatment of functor name (!?) *)
   162     (fn source =>
   163       ML_Lex.read ("ML_Env.check_functor " ^
   164         ML_Syntax.print_string (Input.source_content source))) #>
   165 
   166   ml_text @{binding ML_text} (K []));
   167 
   168 end;
   169 
   170 
   171 (* URLs *)
   172 
   173 val _ = Theory.setup
   174   (Thy_Output.antiquotation @{binding url} (Scan.lift (Parse.position Parse.name))
   175     (fn {context = ctxt, ...} => fn (name, pos) =>
   176       (Context_Position.reports ctxt [(pos, Markup.language_path), (pos, Markup.url name)];
   177        enclose "\\url{" "}" name)));
   178 
   179 
   180 (* doc entries *)
   181 
   182 val _ = Theory.setup
   183   (Thy_Output.antiquotation @{binding doc} (Scan.lift (Parse.position Parse.name))
   184     (fn {context = ctxt, ...} => fn (name, pos) =>
   185       (Context_Position.report ctxt pos (Markup.doc name);
   186         Thy_Output.output ctxt [Thy_Output.pretty_text ctxt name])));
   187 
   188 
   189 (* formal entities *)
   190 
   191 fun entity_antiquotation name check output =
   192   Thy_Output.antiquotation name (Scan.lift (Parse.position Args.name))
   193     (fn {context = ctxt, ...} => fn (name, pos) => (check ctxt (name, pos); output name));
   194 
   195 val _ =
   196   Theory.setup
   197    (entity_antiquotation @{binding command} Outer_Syntax.check_command
   198      (enclose "\\isacommand{" "}" o Output.output) #>
   199     entity_antiquotation @{binding method} Method.check_name Output.output #>
   200     entity_antiquotation @{binding attribute} Attrib.check_name Output.output);
   201 
   202 end;