forked from Isabelle_DOF/Isabelle_DOF
Ad-hoc port to development version of Isabelle.
This commit is contained in:
parent
6a94728747
commit
f40d33b9ed
|
@ -1,7 +1,7 @@
|
||||||
(*************************************************************************
|
(*************************************************************************
|
||||||
* Copyright (C)
|
* Copyright (C)
|
||||||
* 2019 The University of Exeter
|
* 2019-2022 The University of Exeter
|
||||||
* 2018-2019 The University of Paris-Saclay
|
* 2018-2022 The University of Paris-Saclay
|
||||||
* 2018 The University of Sheffield
|
* 2018 The University of Sheffield
|
||||||
*
|
*
|
||||||
* License:
|
* License:
|
||||||
|
@ -1947,6 +1947,23 @@ fun document_output {markdown: bool, markup: Latex.text -> Latex.text} meta_args
|
||||||
val output_text = Document_Output.output_document ctxt {markdown = markdown} text;
|
val output_text = Document_Output.output_document ctxt {markdown = markdown} text;
|
||||||
in markup (output_meta @ output_text) end;
|
in markup (output_meta @ output_text) end;
|
||||||
|
|
||||||
|
val output_name = (* was available as Latex.output_name in Isabelle 2021-1 and earlier *)
|
||||||
|
translate_string
|
||||||
|
(fn "_" => "UNDERSCORE"
|
||||||
|
| "'" => "PRIME"
|
||||||
|
| "0" => "ZERO"
|
||||||
|
| "1" => "ONE"
|
||||||
|
| "2" => "TWO"
|
||||||
|
| "3" => "THREE"
|
||||||
|
| "4" => "FOUR"
|
||||||
|
| "5" => "FIVE"
|
||||||
|
| "6" => "SIX"
|
||||||
|
| "7" => "SEVEN"
|
||||||
|
| "8" => "EIGHT"
|
||||||
|
| "9" => "NINE"
|
||||||
|
| s => s);
|
||||||
|
|
||||||
|
|
||||||
fun document_output_reports name {markdown, body} meta_args text ctxt =
|
fun document_output_reports name {markdown, body} meta_args text ctxt =
|
||||||
let
|
let
|
||||||
val pos = Input.pos_of text;
|
val pos = Input.pos_of text;
|
||||||
|
@ -1956,7 +1973,7 @@ fun document_output_reports name {markdown, body} meta_args text ctxt =
|
||||||
(pos, Markup.plain_text)];
|
(pos, Markup.plain_text)];
|
||||||
fun markup xml =
|
fun markup xml =
|
||||||
let val m = if body then Markup.latex_body else Markup.latex_heading
|
let val m = if body then Markup.latex_body else Markup.latex_heading
|
||||||
in [XML.Elem (m (Latex.output_name name), xml)] end;
|
in [XML.Elem (m (output_name name), xml)] end;
|
||||||
in document_output {markdown = markdown, markup = markup} meta_args text ctxt end;
|
in document_output {markdown = markdown, markup = markup} meta_args text ctxt end;
|
||||||
|
|
||||||
|
|
||||||
|
@ -2332,7 +2349,7 @@ val docitem_modes = Scan.optional (Args.parens (Args.$$$ defineN || Args.$$$ unc
|
||||||
{unchecked = false, define= false} (* default *);
|
{unchecked = false, define= false} (* default *);
|
||||||
|
|
||||||
|
|
||||||
val docitem_antiquotation_parser = (Scan.lift (docitem_modes -- Args.text_input))
|
val docitem_antiquotation_parser = (Scan.lift (docitem_modes -- Parse.embedded_input))
|
||||||
: ({define:bool,unchecked:bool} * Input.source) context_parser;
|
: ({define:bool,unchecked:bool} * Input.source) context_parser;
|
||||||
|
|
||||||
|
|
||||||
|
@ -2781,7 +2798,7 @@ fun string_2_theory_text_antiquotation ctxt text =
|
||||||
end
|
end
|
||||||
|
|
||||||
fun gen_text_antiquotation name reportNcheck compile =
|
fun gen_text_antiquotation name reportNcheck compile =
|
||||||
Document_Output.antiquotation_raw_embedded name (Scan.lift Args.text_input)
|
Document_Output.antiquotation_raw_embedded name (Scan.lift Parse.embedded_input)
|
||||||
(fn ctxt => fn text:Input.source =>
|
(fn ctxt => fn text:Input.source =>
|
||||||
let
|
let
|
||||||
val _ = reportNcheck ctxt text;
|
val _ = reportNcheck ctxt text;
|
||||||
|
@ -2832,12 +2849,11 @@ fun theory_text_antiquotation name =
|
||||||
|
|
||||||
|
|
||||||
fun environment_delim name =
|
fun environment_delim name =
|
||||||
("%\n\\begin{" ^ Latex.output_name name ^ "}\n",
|
("%\n\\begin{" ^ Monitor_Command_Parser.output_name name ^ "}\n",
|
||||||
"\n\\end{" ^ Latex.output_name name ^ "}");
|
"\n\\end{" ^ Monitor_Command_Parser.output_name name ^ "}");
|
||||||
|
|
||||||
fun environment_block name = environment_delim name |-> XML.enclose;
|
fun environment_block name = environment_delim name |-> XML.enclose;
|
||||||
|
|
||||||
|
|
||||||
fun enclose_env verbatim ctxt block_env body =
|
fun enclose_env verbatim ctxt block_env body =
|
||||||
if Config.get ctxt Document_Antiquotation.thy_output_display
|
if Config.get ctxt Document_Antiquotation.thy_output_display
|
||||||
then if verbatim
|
then if verbatim
|
||||||
|
@ -2848,6 +2864,7 @@ fun enclose_env verbatim ctxt block_env body =
|
||||||
end
|
end
|
||||||
\<close>
|
\<close>
|
||||||
|
|
||||||
|
|
||||||
ML\<open>
|
ML\<open>
|
||||||
local
|
local
|
||||||
val parse_literal = Parse.alt_string || Parse.cartouche
|
val parse_literal = Parse.alt_string || Parse.cartouche
|
||||||
|
|
Loading…
Reference in New Issue