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