src/Pure/Thy/document_antiquotations.ML

+(*  Title:      Pure/ML/document_antiquotations.ML
+    Author:     Makarius
+
+Miscellaneous document antiquotations.
+*)
+
+structure Document_Antiquotations: sig end =
+struct
+
+(* control spacing *)
+
+val _ =
+  Theory.setup
+   (Thy_Output.antiquotation @{binding noindent} (Scan.succeed ()) (fn _ => fn () => "\\noindent") #>
+    Thy_Output.antiquotation @{binding smallskip} (Scan.succeed ()) (fn _ => fn () => "\\smallskip") #>
+    Thy_Output.antiquotation @{binding medskip} (Scan.succeed ()) (fn _ => fn () => "\\medskip") #>
+    Thy_Output.antiquotation @{binding bigskip} (Scan.succeed ()) (fn _ => fn () => "\\bigskip"));
+
+
+(* control style *)
+
+local
+
+fun control_antiquotation name s1 s2 =
+  Thy_Output.antiquotation name (Scan.lift Args.cartouche_input)
+    (fn {state, ...} => enclose s1 s2 o Thy_Output.output_text state {markdown = false});
+
+in
+
+val _ =
+  Theory.setup
+   (control_antiquotation @{binding footnote} "\\footnote{" "}" #>
+    control_antiquotation @{binding emph} "\\emph{" "}" #>
+    control_antiquotation @{binding bold} "\\textbf{" "}");
+
+end;
+
+
+(* quasi-formal text (unchecked) *)
+
+local
+
+fun text_antiquotation name =
+  Thy_Output.antiquotation name (Scan.lift Args.text_input)
+    (fn {context = ctxt, ...} => fn source =>
+     (Context_Position.report ctxt (Input.pos_of source)
+        (Markup.language_text (Input.is_delimited source));
+      Thy_Output.output ctxt [Thy_Output.pretty_text ctxt (Input.source_content source)]));
+
+in
+
+val _ =
+  Theory.setup
+   (text_antiquotation @{binding text} #>
+    text_antiquotation @{binding cartouche});
+
+end;
+
+
+(* theory text with tokens (unchecked) *)
+
+val _ =
+  Theory.setup
+    (Thy_Output.antiquotation @{binding theory_text} (Scan.lift Args.text_input)
+      (fn {context = ctxt, ...} => fn source =>
+        let
+          val _ =
+            Context_Position.report ctxt (Input.pos_of source)
+              (Markup.language_outer (Input.is_delimited source));
+
+          val keywords = Thy_Header.get_keywords' ctxt;
+          val toks =
+            Source.of_list (Input.source_explode source)
+            |> Token.source' true keywords
+            |> Source.exhaust;
+          val _ = Context_Position.reports_text ctxt (maps (Token.reports keywords) toks);
+        in
+          implode (map Latex.output_token toks) |>
+           (if Config.get ctxt Thy_Output.display
+            then Latex.environment "isabelle"
+            else enclose "\\isa{" "}")
+        end));
+
+
+(* goal state *)
+
+local
+
+fun goal_state name main = Thy_Output.antiquotation name (Scan.succeed ())
+  (fn {state, context = ctxt, ...} => fn () =>
+    Thy_Output.output ctxt
+      [Goal_Display.pretty_goal
+        (Config.put Goal_Display.show_main_goal main ctxt)
+        (#goal (Proof.goal (Toplevel.proof_of state)))]);
+
+in
+
+val _ = Theory.setup
+ (goal_state @{binding goals} true #>
+  goal_state @{binding subgoals} false);
+
+end;
+
+
+(* embedded lemma *)
+
+val _ = Theory.setup
+  (Thy_Output.antiquotation @{binding lemma}
+    (Scan.lift (Scan.ahead Parse.not_eof) -- Args.prop --
+      Scan.lift (Parse.position (Parse.reserved "by") -- Method.parse -- Scan.option Method.parse))
+    (fn {source, context = ctxt, ...} => fn ((prop_token, prop), (((_, by_pos), m1), m2)) =>
+      let
+        val prop_src = Token.src (Token.name_of_src source) [prop_token];
+
+        val reports = (by_pos, Markup.keyword1) :: maps Method.reports_of (m1 :: the_list m2);
+        val _ = Context_Position.reports ctxt reports;
+
+        (* FIXME check proof!? *)
+        val _ = ctxt
+          |> Proof.theorem NONE (K I) [[(prop, [])]]
+          |> Proof.global_terminal_proof (m1, m2);
+      in
+        Thy_Output.output ctxt
+          (Thy_Output.maybe_pretty_source Thy_Output.pretty_term ctxt prop_src [prop])
+      end));
+
+
+(* verbatim text *)
+
+val _ =
+  Theory.setup
+    (Thy_Output.antiquotation @{binding verbatim} (Scan.lift Args.text)
+      (Thy_Output.verbatim_text o #context));
+
+
+(* ML text *)
+
+local
+
+fun ml_text name ml = Thy_Output.antiquotation name (Scan.lift Args.text_input)
+  (fn {context = ctxt, ...} => fn source =>
+   (ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (Input.pos_of source) (ml source);
+    Thy_Output.verbatim_text ctxt (Input.source_content source)));
+
+fun ml_enclose bg en source =
+  ML_Lex.read bg @ ML_Lex.read_source false source @ ML_Lex.read en;
+
+in
+
+val _ = Theory.setup
+ (ml_text @{binding ML} (ml_enclose "fn _ => (" ");") #>
+  ml_text @{binding ML_op} (ml_enclose "fn _ => (op " ");") #>
+  ml_text @{binding ML_type} (ml_enclose "val _ = NONE : (" ") option;") #>
+  ml_text @{binding ML_structure}
+    (ml_enclose "functor XXX() = struct structure XX = " " end;") #>
+
+  ml_text @{binding ML_functor}   (* FIXME formal treatment of functor name (!?) *)
+    (fn source =>
+      ML_Lex.read ("ML_Env.check_functor " ^
+        ML_Syntax.print_string (Input.source_content source))) #>
+
+  ml_text @{binding ML_text} (K []));
+
+end;
+
+
+(* URLs *)
+
+val _ = Theory.setup
+  (Thy_Output.antiquotation @{binding url} (Scan.lift (Parse.position Parse.name))
+    (fn {context = ctxt, ...} => fn (name, pos) =>
+      (Context_Position.reports ctxt [(pos, Markup.language_path), (pos, Markup.url name)];
+       enclose "\\url{" "}" name)));
+
+end;