--- a/etc/symbols Fri Jan 19 15:50:17 2018 +0100
+++ b/etc/symbols Fri Jan 19 20:11:14 2018 +0100
@@ -410,6 +410,7 @@
\<^plugin> argument: cartouche
\<^print>
\<^prop> argument: cartouche
+\<^session> argument: cartouche
\<^simproc> argument: cartouche
\<^sort> argument: cartouche
\<^syntax_const> argument: cartouche
--- a/src/Doc/Isar_Ref/Outer_Syntax.thy Fri Jan 19 15:50:17 2018 +0100
+++ b/src/Doc/Isar_Ref/Outer_Syntax.thy Fri Jan 19 20:11:14 2018 +0100
@@ -255,8 +255,8 @@
document preparation (\chref{ch:document-prep}) supports various styles,
according to the following kinds of comments.
- \<^item> Marginal comment of the form \<^verbatim>\<open>\<comment>\<close>~\<open>\<open>text\<close>\<close> or \<open>\<comment> \<open>text\<close>\<close>, usually with a
- single space between the comment symbol and the argument cartouche. The
+ \<^item> Marginal comment of the form \<^verbatim>\<open>\<comment>\<close>~\<open>\<open>text\<close>\<close> or \<open>\<comment>\<close>~\<open>\<open>text\<close>\<close>, usually with
+ a single space between the comment symbol and the argument cartouche. The
given argument is typeset as regular text, with formal antiquotations
(\secref{sec:antiq}).
--- a/src/Doc/Main/Main_Doc.thy Fri Jan 19 15:50:17 2018 +0100
+++ b/src/Doc/Main/Main_Doc.thy Fri Jan 19 20:11:14 2018 +0100
@@ -4,23 +4,15 @@
begin
setup \<open>
- let
- fun pretty_term_type_only ctxt (t, T) =
+ Thy_Output.antiquotation_pretty_source @{binding term_type_only} (Args.term -- Args.typ_abbrev)
+ (fn ctxt => fn (t, T) =>
(if fastype_of t = Sign.certify_typ (Proof_Context.theory_of ctxt) T then ()
else error "term_type_only: type mismatch";
- Syntax.pretty_typ ctxt T)
- in
- Document_Antiquotation.setup @{binding term_type_only}
- (Args.term -- Args.typ_abbrev)
- (fn {source, context = ctxt, ...} => fn arg =>
- Thy_Output.output ctxt
- (Thy_Output.maybe_pretty_source pretty_term_type_only ctxt source [arg]))
- end
+ [Syntax.pretty_typ ctxt T]))
\<close>
setup \<open>
- Document_Antiquotation.setup @{binding expanded_typ} (Args.typ >> single)
- (fn {source, context, ...} => Thy_Output.output context o
- Thy_Output.maybe_pretty_source Syntax.pretty_typ context source)
+ Thy_Output.antiquotation_pretty_source @{binding expanded_typ} Args.typ
+ (fn ctxt => fn T => [Syntax.pretty_typ ctxt T])
\<close>
(*>*)
text\<open>
--- a/src/Doc/Prog_Prove/LaTeXsugar.thy Fri Jan 19 15:50:17 2018 +0100
+++ b/src/Doc/Prog_Prove/LaTeXsugar.thy Fri Jan 19 20:11:14 2018 +0100
@@ -43,20 +43,13 @@
"_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^latex>\<open>{\\normalsize \\,\<close>and\<^latex>\<open>\\,}\<close>/ _")
"_asm" :: "prop \<Rightarrow> asms" ("_")
-setup\<open>
- let
- fun pretty ctxt c =
- let val tc = Proof_Context.read_const {proper = true, strict = false} ctxt c
- in Pretty.block [Thy_Output.pretty_term ctxt tc, Pretty.str " ::",
- Pretty.brk 1, Syntax.pretty_typ ctxt (fastype_of tc)]
- end
- in
- Document_Antiquotation.setup @{binding "const_typ"}
- (Scan.lift Args.embedded_inner_syntax)
- (fn {source = src, context = ctxt, ...} => fn arg =>
- Thy_Output.output ctxt
- (Thy_Output.maybe_pretty_source pretty ctxt src [arg]))
- end;
+setup \<open>
+ Thy_Output.antiquotation_pretty_source \<^binding>\<open>const_typ\<close> (Scan.lift Args.embedded_inner_syntax)
+ (fn ctxt => fn c =>
+ let val tc = Proof_Context.read_const {proper = true, strict = false} ctxt c in
+ [Pretty.block [Thy_Output.pretty_term ctxt tc, Pretty.str " ::",
+ Pretty.brk 1, Syntax.pretty_typ ctxt (fastype_of tc)]]
+ end)
\<close>
end
--- a/src/Doc/antiquote_setup.ML Fri Jan 19 15:50:17 2018 +0100
+++ b/src/Doc/antiquote_setup.ML Fri Jan 19 20:11:14 2018 +0100
@@ -73,9 +73,9 @@
fun prep_ml source =
(Input.source_content source, ML_Lex.read_source false source);
-fun index_ml name kind ml = Document_Antiquotation.setup name
+fun index_ml name kind ml = Thy_Output.antiquotation_raw name
(Scan.lift (Args.text_input -- Scan.option (Args.colon |-- Args.text_input)))
- (fn {context = ctxt, ...} => fn (source1, opt_source2) =>
+ (fn ctxt => fn (source1, opt_source2) =>
let
val (txt1, toks1) = prep_ml source1;
val (txt2, toks2) =
@@ -98,8 +98,9 @@
handle ERROR msg => error (msg ^ Position.here pos);
val kind' = if kind = "" then "ML" else "ML " ^ kind;
in
- "\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string (ml_name txt1) ^ "}" ^
- (Thy_Output.verbatim_text ctxt txt')
+ Latex.block
+ [Latex.string ("\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string (ml_name txt1) ^ "}"),
+ Thy_Output.verbatim ctxt txt']
end);
in
@@ -119,29 +120,17 @@
(* named theorems *)
val _ =
- Theory.setup (Document_Antiquotation.setup @{binding named_thms}
+ Theory.setup (Thy_Output.antiquotation_raw @{binding named_thms}
(Scan.repeat (Attrib.thm -- Scan.lift (Args.parens Args.name)))
- (fn {context = ctxt, ...} =>
- map (apfst (Thy_Output.pretty_thm ctxt))
- #> (if Config.get ctxt Document_Antiquotation.thy_output_quotes
- then map (apfst Pretty.quote) else I)
- #> (if Config.get ctxt Document_Antiquotation.thy_output_display
- then
- map (fn (p, name) =>
- Output.output
- (Thy_Output.string_of_margin ctxt
- (Pretty.indent (Config.get ctxt Document_Antiquotation.thy_output_indent) p)) ^
- "\\rulename{" ^
- Output.output (Pretty.unformatted_string_of (Thy_Output.pretty_text ctxt name)) ^ "}")
- #> space_implode "\\par\\smallskip%\n"
- #> Latex.environment "isabelle"
- else
- map (fn (p, name) =>
- Output.output (Pretty.unformatted_string_of p) ^
- "\\rulename{" ^
- Output.output (Pretty.unformatted_string_of (Thy_Output.pretty_text ctxt name)) ^ "}")
- #> space_implode "\\par\\smallskip%\n"
- #> enclose "\\isa{" "}")));
+ (fn ctxt =>
+ map (fn (thm, name) =>
+ Output.output
+ (Document_Antiquotation.format ctxt
+ (Document_Antiquotation.quote ctxt (Thy_Output.pretty_thm ctxt thm))) ^
+ enclose "\\rulename{" "}" (Output.output name))
+ #> space_implode "\\par\\smallskip%\n"
+ #> Latex.string #> single
+ #> Thy_Output.isabelle ctxt));
(* Isabelle/Isar entities (with index) *)
@@ -161,11 +150,11 @@
val arg = enclose "{" "}" o clean_string;
fun entity check markup binding index =
- Document_Antiquotation.setup
+ Thy_Output.antiquotation_raw
(binding |> Binding.map_name (fn name => name ^
(case index of NONE => "" | SOME true => "_def" | SOME false => "_ref")))
(Scan.lift (Scan.optional (Args.parens Args.name) "" -- Parse.position Args.name))
- (fn {context = ctxt, ...} => fn (logic, (name, pos)) =>
+ (fn ctxt => fn (logic, (name, pos)) =>
let
val kind = translate (fn "_" => " " | c => c) (Binding.name_of binding);
val hyper_name =
@@ -180,12 +169,12 @@
"\\index" ^ (if is_def then "def" else "ref") ^ arg logic ^ arg kind ^ arg name);
val _ =
if Context_Position.is_reported ctxt pos then ignore (check ctxt (name, pos)) else ();
- in
- idx ^
- (Output.output name
- |> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}")
- |> hyper o enclose "\\mbox{\\isa{" "}}")
- end);
+ val latex =
+ idx ^
+ (Output.output name
+ |> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}")
+ |> hyper o enclose "\\mbox{\\isa{" "}}");
+ in Latex.string latex end);
fun entity_antiqs check markup kind =
entity check markup kind NONE #>
--- a/src/Doc/more_antiquote.ML Fri Jan 19 15:50:17 2018 +0100
+++ b/src/Doc/more_antiquote.ML Fri Jan 19 20:11:14 2018 +0100
@@ -9,53 +9,37 @@
(* class specifications *)
-local
-
-fun class_spec ctxt s =
- let
- val thy = Proof_Context.theory_of ctxt;
- val class = Sign.intern_class thy s;
- in Thy_Output.output ctxt (Class.pretty_specification thy class) end;
-
-in
-
val _ =
- Theory.setup (Document_Antiquotation.setup @{binding class_spec} (Scan.lift Args.name)
- (fn {context, ...} => class_spec context));
-
-end;
+ Theory.setup (Thy_Output.antiquotation_pretty @{binding class_spec} (Scan.lift Args.name)
+ (fn ctxt => fn s =>
+ let
+ val thy = Proof_Context.theory_of ctxt;
+ val class = Sign.intern_class thy s;
+ in Class.pretty_specification thy class end));
(* code theorem antiquotation *)
-local
-
fun no_vars ctxt thm =
let
val ctxt' = Variable.set_body false ctxt;
val ((_, [thm]), _) = Variable.import true [thm] ctxt';
in thm end;
-fun pretty_code_thm ctxt raw_const =
- let
- val thy = Proof_Context.theory_of ctxt;
- val const = Code.check_const thy raw_const;
- val { eqngr, ... } = Code_Preproc.obtain true { ctxt = ctxt, consts = [const], terms = [] };
- fun holize thm = @{thm meta_eq_to_obj_eq} OF [thm];
- val thms = Code_Preproc.cert eqngr const
- |> Code.equations_of_cert thy
- |> snd
- |> these
- |> map_filter (fn (_, (some_thm, proper)) => if proper then some_thm else NONE)
- |> map (holize o no_vars ctxt o Axclass.overload ctxt);
- in Thy_Output.output ctxt (map (Thy_Output.pretty_thm ctxt) thms) end;
-
-in
-
val _ =
- Theory.setup (Document_Antiquotation.setup @{binding code_thms} Args.term
- (fn {context, ...} => pretty_code_thm context));
+ Theory.setup (Thy_Output.antiquotation_pretty @{binding code_thms} Args.term
+ (fn ctxt => fn raw_const =>
+ let
+ val thy = Proof_Context.theory_of ctxt;
+ val const = Code.check_const thy raw_const;
+ val { eqngr, ... } = Code_Preproc.obtain true { ctxt = ctxt, consts = [const], terms = [] };
+ fun holize thm = @{thm meta_eq_to_obj_eq} OF [thm];
+ val thms = Code_Preproc.cert eqngr const
+ |> Code.equations_of_cert thy
+ |> snd
+ |> these
+ |> map_filter (fn (_, (some_thm, proper)) => if proper then some_thm else NONE)
+ |> map (holize o no_vars ctxt o Axclass.overload ctxt);
+ in map (Thy_Output.pretty_thm ctxt) thms end));
end;
-
-end;
--- a/src/HOL/Library/LaTeXsugar.thy Fri Jan 19 15:50:17 2018 +0100
+++ b/src/HOL/Library/LaTeXsugar.thy Fri Jan 19 20:11:14 2018 +0100
@@ -96,20 +96,13 @@
"_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^latex>\<open>{\\normalsize \\,\<close>and\<^latex>\<open>\\,}\<close>/ _")
"_asm" :: "prop \<Rightarrow> asms" ("_")
-setup\<open>
- let
- fun pretty ctxt c =
- let val tc = Proof_Context.read_const {proper = true, strict = false} ctxt c
- in Pretty.block [Thy_Output.pretty_term ctxt tc, Pretty.str " ::",
- Pretty.brk 1, Syntax.pretty_typ ctxt (fastype_of tc)]
- end
- in
- Document_Antiquotation.setup @{binding "const_typ"}
- (Scan.lift Args.embedded_inner_syntax)
- (fn {source = src, context = ctxt, ...} => fn arg =>
- Thy_Output.output ctxt
- (Thy_Output.maybe_pretty_source pretty ctxt src [arg]))
- end;
+setup \<open>
+ Thy_Output.antiquotation_pretty_source \<^binding>\<open>const_typ\<close> (Scan.lift Args.embedded_inner_syntax)
+ (fn ctxt => fn c =>
+ let val tc = Proof_Context.read_const {proper = true, strict = false} ctxt c in
+ [Pretty.block [Thy_Output.pretty_term ctxt tc, Pretty.str " ::",
+ Pretty.brk 1, Syntax.pretty_typ ctxt (fastype_of tc)]]
+ end)
\<close>
setup\<open>
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML Fri Jan 19 15:50:17 2018 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Fri Jan 19 20:11:14 2018 +0100
@@ -983,8 +983,8 @@
end;
fun fp_antiquote_setup binding =
- Document_Antiquotation.setup binding (Args.type_name {proper = true, strict = true})
- (fn {source = src, context = ctxt, ...} => fn fcT_name =>
+ Thy_Output.antiquotation_pretty_source binding (Args.type_name {proper = true, strict = true})
+ (fn ctxt => fn fcT_name =>
(case Ctr_Sugar.ctr_sugar_of ctxt fcT_name of
NONE => error ("Not a known freely generated type name: " ^ quote fcT_name)
| SOME {T = T0, ctrs = ctrs0, ...} =>
@@ -1002,9 +1002,6 @@
Pretty.block (Pretty.keyword1 (Binding.name_of binding) :: Pretty.brk 1 ::
Syntax.pretty_typ ctxt T :: Pretty.str " =" :: Pretty.brk 1 ::
flat (separate [Pretty.brk 1, Pretty.str "| "] (map (single o pretty_ctr) ctrs)));
- in
- Thy_Output.output ctxt
- (Thy_Output.maybe_pretty_source (K (K pretty_co_datatype)) ctxt src [()])
- end));
+ in [pretty_co_datatype] end));
end;
--- a/src/HOL/Tools/value_command.ML Fri Jan 19 15:50:17 2018 +0100
+++ b/src/HOL/Tools/value_command.ML Fri Jan 19 20:11:14 2018 +0100
@@ -73,11 +73,10 @@
>> (fn ((name, modes), t) => Toplevel.keep (value_cmd name modes t)));
val _ = Theory.setup
- (Document_Antiquotation.setup \<^binding>\<open>value\<close>
+ (Thy_Output.antiquotation_pretty_source \<^binding>\<open>value\<close>
(Scan.lift opt_evaluator -- Term_Style.parse -- Args.term)
- (fn {source, context, ...} => fn ((name, style), t) => Thy_Output.output context
- (Thy_Output.maybe_pretty_source Thy_Output.pretty_term context source
- [style (value_select name context t)]))
+ (fn ctxt => fn ((name, style), t) =>
+ [Thy_Output.pretty_term ctxt (style (value_select name ctxt t))])
#> add_evaluator (\<^binding>\<open>simp\<close>, Code_Simp.dynamic_value) #> snd
#> add_evaluator (\<^binding>\<open>nbe\<close>, Nbe.dynamic_value) #> snd
#> add_evaluator (\<^binding>\<open>code\<close>, Code_Evaluation.dynamic_value_strict) #> snd);
--- a/src/Pure/General/antiquote.ML Fri Jan 19 15:50:17 2018 +0100
+++ b/src/Pure/General/antiquote.ML Fri Jan 19 20:11:14 2018 +0100
@@ -10,7 +10,8 @@
type antiq = {start: Position.T, stop: Position.T, range: Position.range, body: Symbol_Pos.T list}
datatype 'a antiquote = Text of 'a | Control of control | Antiq of antiq
type text_antiquote = Symbol_Pos.T list antiquote
- val range: text_antiquote list -> Position.range
+ val text_antiquote_range: text_antiquote -> Position.range
+ val text_range: text_antiquote list -> Position.range
val split_lines: text_antiquote list -> text_antiquote list list
val antiq_reports: 'a antiquote list -> Position.report list
val scan_control: control scanner
@@ -31,13 +32,14 @@
type text_antiquote = Symbol_Pos.T list antiquote;
-fun antiquote_range (Text ss) = Symbol_Pos.range ss
- | antiquote_range (Control {range, ...}) = range
- | antiquote_range (Antiq {range, ...}) = range;
+fun text_antiquote_range (Text ss) = Symbol_Pos.range ss
+ | text_antiquote_range (Control {range, ...}) = range
+ | text_antiquote_range (Antiq {range, ...}) = range;
-fun range ants =
+fun text_range ants =
if null ants then Position.no_range
- else Position.range (#1 (antiquote_range (hd ants)), #2 (antiquote_range (List.last ants)));
+ else
+ Position.range (#1 (text_antiquote_range (hd ants)), #2 (text_antiquote_range (List.last ants)));
(* split lines *)
--- a/src/Pure/General/symbol_pos.ML Fri Jan 19 15:50:17 2018 +0100
+++ b/src/Pure/General/symbol_pos.ML Fri Jan 19 20:11:14 2018 +0100
@@ -11,9 +11,6 @@
val symbol: T -> Symbol.symbol
val content: T list -> string
val range: T list -> Position.range
- val split_lines: T list -> T list list
- val trim_blanks: T list -> T list
- val trim_lines: T list -> T list
val is_eof: T -> bool
val stopper: T Scan.stopper
val !!! : Scan.message -> 'a scanner -> 'a scanner
@@ -69,23 +66,6 @@
| range [] = Position.no_range;
-(* lines and blanks *)
-
-fun split_lines [] = []
- | split_lines (list: T list) =
- let
- fun split syms =
- (case take_prefix (fn (s, _) => s <> "\n") syms of
- (line, []) => [line]
- | (line, _ :: rest) => line :: split rest);
- in split list end;
-
-val trim_blanks = trim (Symbol.is_blank o symbol);
-
-val trim_lines =
- split_lines #> map trim_blanks #> separate [(Symbol.space, Position.none)] #> flat;
-
-
(* stopper *)
fun mk_eof pos = (Symbol.eof, pos);
--- a/src/Pure/ML/ml_process.scala Fri Jan 19 15:50:17 2018 +0100
+++ b/src/Pure/ML/ml_process.scala Fri Jan 19 20:11:14 2018 +0100
@@ -103,6 +103,7 @@
ML_Syntax.print_list(ML_Syntax.print_string_bytes)(list)
List("Resources.init_session_base" +
" {sessions = " + print_list(base.known.sessions.toList) +
+ ", doc_names = " + print_list(base.doc_names) +
", global_theories = " + print_table(base.global_theories.toList) +
", loaded_theories = " + print_list(base.loaded_theories.keys) +
", known_theories = " + print_table(base.dest_known_theories) + "}")
--- a/src/Pure/PIDE/protocol.ML Fri Jan 19 15:50:17 2018 +0100
+++ b/src/Pure/PIDE/protocol.ML Fri Jan 19 20:11:14 2018 +0100
@@ -19,13 +19,15 @@
val _ =
Isabelle_Process.protocol_command "Prover.init_session_base"
- (fn [sessions_yxml, global_theories_yxml, loaded_theories_yxml, known_theories_yxml] =>
+ (fn [sessions_yxml, doc_names_yxml, global_theories_yxml, loaded_theories_yxml,
+ known_theories_yxml] =>
let
val decode_table = YXML.parse_body #> let open XML.Decode in list (pair string string) end;
val decode_list = YXML.parse_body #> let open XML.Decode in list string end;
in
Resources.init_session_base
{sessions = decode_list sessions_yxml,
+ doc_names = decode_list doc_names_yxml,
global_theories = decode_table global_theories_yxml,
loaded_theories = decode_list loaded_theories_yxml,
known_theories = decode_table known_theories_yxml}
--- a/src/Pure/PIDE/protocol.scala Fri Jan 19 15:50:17 2018 +0100
+++ b/src/Pure/PIDE/protocol.scala Fri Jan 19 20:11:14 2018 +0100
@@ -343,6 +343,7 @@
val base = resources.session_base.standard_path
protocol_command("Prover.init_session_base",
encode_list(base.known.sessions.toList),
+ encode_list(base.doc_names),
encode_table(base.global_theories.toList),
encode_list(base.loaded_theories.keys),
encode_table(base.dest_known_theories))
--- a/src/Pure/PIDE/resources.ML Fri Jan 19 15:50:17 2018 +0100
+++ b/src/Pure/PIDE/resources.ML Fri Jan 19 20:11:14 2018 +0100
@@ -9,6 +9,7 @@
val default_qualifier: string
val init_session_base:
{sessions: string list,
+ doc_names: string list,
global_theories: (string * string) list,
loaded_theories: string list,
known_theories: (string * string) list} -> unit
@@ -17,6 +18,7 @@
val loaded_theory: string -> bool
val known_theory: string -> Path.T option
val check_session: Proof.context -> string * Position.T -> string
+ val check_doc: Proof.context -> string * Position.T -> string
val master_directory: theory -> Path.T
val imports_of: theory -> (string * Position.T) list
val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory
@@ -45,6 +47,7 @@
val empty_session_base =
{sessions = []: string list,
+ doc_names = []: string list,
global_theories = Symtab.empty: string Symtab.table,
loaded_theories = Symtab.empty: unit Symtab.table,
known_theories = Symtab.empty: Path.T Symtab.table};
@@ -52,10 +55,11 @@
val global_session_base =
Synchronized.var "Sessions.base" empty_session_base;
-fun init_session_base {sessions, global_theories, loaded_theories, known_theories} =
+fun init_session_base {sessions, doc_names, global_theories, loaded_theories, known_theories} =
Synchronized.change global_session_base
(fn _ =>
{sessions = sort_strings sessions,
+ doc_names = doc_names,
global_theories = Symtab.make global_theories,
loaded_theories = Symtab.make_set loaded_theories,
known_theories = Symtab.make (map (apsnd Path.explode) known_theories)});
@@ -64,6 +68,7 @@
Synchronized.change global_session_base
(fn {global_theories, loaded_theories, ...} =>
{sessions = [],
+ doc_names = [],
global_theories = global_theories,
loaded_theories = loaded_theories,
known_theories = #known_theories empty_session_base});
@@ -74,21 +79,26 @@
fun loaded_theory a = Symtab.defined (get_session_base #loaded_theories) a;
fun known_theory a = Symtab.lookup (get_session_base #known_theories) a;
-fun check_session ctxt (name, pos) =
- let val sessions = get_session_base #sessions in
- if member (op =) sessions name then
- (Context_Position.report ctxt pos (Markup.entity Markup.sessionN name); name)
+fun check_name which kind markup ctxt (name, pos) =
+ let val names = get_session_base which in
+ if member (op =) names name then
+ (Context_Position.report ctxt pos (markup name); name)
else
let
val completion =
Completion.make (name, pos) (fn completed =>
- sessions
+ names
|> filter completed
- |> map (fn a => (a, (Markup.sessionN, a))));
+ |> sort_strings
+ |> map (fn a => (a, (kind, a))));
val report = Markup.markup_report (Completion.reported_text completion);
- in error ("Bad session " ^ quote name ^ Position.here pos ^ report) end
+ in error ("Bad " ^ kind ^ " " ^ quote name ^ Position.here pos ^ report) end
end;
+val check_session = check_name #sessions "session" (Markup.entity Markup.sessionN);
+val check_doc = check_name #doc_names "documentation" Markup.doc;
+
+
(* manage source files *)
@@ -243,12 +253,11 @@
let
val dir = master_directory (Proof_Context.theory_of ctxt);
val _ = check ctxt dir (name, pos);
- in
- space_explode "/" name
- |> map Latex.output_ascii
- |> space_implode (Latex.output_ascii "/" ^ "\\discretionary{}{}{}")
- |> enclose "\\isatt{" "}"
- end;
+ val latex =
+ space_explode "/" name
+ |> map Latex.output_ascii
+ |> space_implode (Latex.output_ascii "/" ^ "\\discretionary{}{}{}");
+ in Latex.enclose_block "\\isatt{" "}" [Latex.string latex] end;
fun ML_antiq check ctxt (name, pos) =
let val path = check ctxt Path.current (name, pos);
@@ -257,14 +266,16 @@
in
val _ = Theory.setup
- (Document_Antiquotation.setup \<^binding>\<open>session\<close> (Scan.lift (Parse.position Parse.embedded))
- (fn {context = ctxt, ...} => Thy_Output.verbatim_text ctxt o check_session ctxt) #>
- Document_Antiquotation.setup \<^binding>\<open>path\<close> (Scan.lift (Parse.position Parse.path))
- (document_antiq check_path o #context) #>
- Document_Antiquotation.setup \<^binding>\<open>file\<close> (Scan.lift (Parse.position Parse.path))
- (document_antiq check_file o #context) #>
- Document_Antiquotation.setup \<^binding>\<open>dir\<close> (Scan.lift (Parse.position Parse.path))
- (document_antiq check_dir o #context) #>
+ (Thy_Output.antiquotation_verbatim \<^binding>\<open>session\<close>
+ (Scan.lift (Parse.position Parse.embedded)) check_session #>
+ Thy_Output.antiquotation_verbatim \<^binding>\<open>doc\<close>
+ (Scan.lift (Parse.position Parse.embedded)) check_doc #>
+ Thy_Output.antiquotation_raw \<^binding>\<open>path\<close>
+ (Scan.lift (Parse.position Parse.path)) (document_antiq check_path) #>
+ Thy_Output.antiquotation_raw \<^binding>\<open>file\<close>
+ (Scan.lift (Parse.position Parse.path)) (document_antiq check_file) #>
+ Thy_Output.antiquotation_raw \<^binding>\<open>dir\<close>
+ (Scan.lift (Parse.position Parse.path)) (document_antiq check_dir) #>
ML_Antiquotation.value \<^binding>\<open>path\<close>
(Args.context -- Scan.lift (Parse.position Parse.path) >> uncurry (ML_antiq check_path)) #>
ML_Antiquotation.value \<^binding>\<open>file\<close>
--- a/src/Pure/Thy/bibtex.ML Fri Jan 19 15:50:17 2018 +0100
+++ b/src/Pure/Thy/bibtex.ML Fri Jan 19 20:11:14 2018 +0100
@@ -41,11 +41,11 @@
val _ =
Theory.setup
(Document_Antiquotation.setup_option \<^binding>\<open>cite_macro\<close> (Config.put cite_macro) #>
- Document_Antiquotation.setup \<^binding>\<open>cite\<close>
+ Thy_Output.antiquotation_raw \<^binding>\<open>cite\<close>
(Scan.lift
(Scan.option (Parse.verbatim || Parse.cartouche) --
Parse.and_list1 (Parse.position Args.name)))
- (fn {context = ctxt, ...} => fn (opt, citations) =>
+ (fn ctxt => fn (opt, citations) =>
let
val thy = Proof_Context.theory_of ctxt;
val bibtex_entries = Present.get_bibtex_entries thy;
@@ -60,6 +60,6 @@
(map (fn (name, pos) => (pos, Markup.citation name)) citations);
val opt_arg = (case opt of NONE => "" | SOME s => "[" ^ s ^ "]");
val arg = "{" ^ space_implode "," (map #1 citations) ^ "}";
- in "\\" ^ Config.get ctxt cite_macro ^ opt_arg ^ arg end));
+ in Latex.string ("\\" ^ Config.get ctxt cite_macro ^ opt_arg ^ arg) end));
end;
--- a/src/Pure/Thy/document_antiquotation.ML Fri Jan 19 15:50:17 2018 +0100
+++ b/src/Pure/Thy/document_antiquotation.ML Fri Jan 19 20:11:14 2018 +0100
@@ -13,16 +13,23 @@
val thy_output_source: bool Config.T
val thy_output_break: bool Config.T
val thy_output_modes: string Config.T
- val add_wrapper: ((unit -> string) -> unit -> string) -> Proof.context -> Proof.context
+ val trim_blanks: Proof.context -> string -> string
+ val trim_lines: Proof.context -> string -> string
+ val indent_lines: Proof.context -> string -> string
+ val prepare_lines: Proof.context -> string -> string
+ val quote: Proof.context -> Pretty.T -> Pretty.T
+ val indent: Proof.context -> Pretty.T -> Pretty.T
+ val format: Proof.context -> Pretty.T -> string
+ val output: Proof.context -> Pretty.T -> Output.output
val print_antiquotations: bool -> Proof.context -> unit
val check: Proof.context -> xstring * Position.T -> string
val check_option: Proof.context -> xstring * Position.T -> string
val setup: binding -> 'a context_parser ->
- ({source: Token.src, context: Proof.context} -> 'a -> string) -> theory -> theory
+ ({context: Proof.context, source: Token.src, argument: 'a} -> Latex.text) -> theory -> theory
val setup_option: binding -> (string -> Proof.context -> Proof.context) -> theory -> theory
val boolean: string -> bool
val integer: string -> int
- val evaluate: Proof.context -> Antiquote.text_antiquote -> string
+ val evaluate: Proof.context -> Antiquote.text_antiquote -> Latex.text list
end;
structure Document_Antiquotation: DOCUMENT_ANTIQUOTATION =
@@ -39,15 +46,38 @@
val thy_output_modes = Attrib.setup_option_string ("thy_output_modes", \<^here>);
-structure Wrappers = Proof_Data
-(
- type T = ((unit -> string) -> unit -> string) list;
- fun init _ = [];
-);
+(* blanks *)
+
+fun trim_blanks ctxt =
+ not (Config.get ctxt thy_output_display) ? Symbol.trim_blanks;
+
+fun trim_lines ctxt =
+ if not (Config.get ctxt thy_output_display) then
+ split_lines #> map Symbol.trim_blanks #> space_implode " "
+ else I;
+
+fun indent_lines ctxt =
+ if Config.get ctxt thy_output_display then
+ prefix_lines (Symbol.spaces (Config.get ctxt thy_output_indent))
+ else I;
-fun add_wrapper wrapper = Wrappers.map (cons wrapper);
+fun prepare_lines ctxt = trim_lines ctxt #> indent_lines ctxt;
+
+
+(* output *)
+
+fun quote ctxt =
+ Config.get ctxt thy_output_quotes ? Pretty.quote;
-val wrap = Wrappers.get #> fold (fn wrapper => fn f => wrapper f);
+fun indent ctxt =
+ Config.get ctxt thy_output_display ? Pretty.indent (Config.get ctxt thy_output_indent);
+
+fun format ctxt =
+ if Config.get ctxt thy_output_display orelse Config.get ctxt thy_output_break
+ then Pretty.string_of_margin (Config.get ctxt thy_output_margin)
+ else Pretty.unformatted_string_of;
+
+fun output ctxt = quote ctxt #> indent ctxt #> format ctxt #> Output.output;
(* theory data *)
@@ -55,7 +85,7 @@
structure Data = Theory_Data
(
type T =
- (Token.src -> Proof.context -> string) Name_Space.table *
+ (Token.src -> Proof.context -> Latex.text) Name_Space.table *
(string -> Proof.context -> Proof.context) Name_Space.table;
val empty : T =
(Name_Space.empty_table Markup.document_antiquotationN,
@@ -85,7 +115,7 @@
let
fun cmd src ctxt =
let val (x, ctxt') = Token.syntax scan src ctxt
- in body {source = src, context = ctxt'} x end;
+ in body {context = ctxt', source = src, argument = x} end;
in thy |> Data.map (apfst (Name_Space.define (Context.Theory thy) true (name, cmd) #> #2)) end;
fun setup_option name opt thy = thy
@@ -104,7 +134,7 @@
in
-val antiq =
+val parse_antiq =
Parse.!!!
(Parse.token Parse.liberal_name -- properties -- Parse.args --| Scan.ahead Parse.eof)
>> (fn ((name, props), args) => (props, name :: args));
@@ -129,21 +159,22 @@
fun eval ctxt (opts, src) =
let
val preview_ctxt = fold option opts ctxt;
- val print_ctxt = Context_Position.set_visible false preview_ctxt;
+ val _ = command src preview_ctxt;
- fun cmd ctxt = wrap ctxt (fn () => command src ctxt) ();
- val _ = cmd preview_ctxt;
+ val print_ctxt = Context_Position.set_visible false preview_ctxt;
val print_modes = space_explode "," (Config.get print_ctxt thy_output_modes) @ [Latex.latexN];
- in Print_Mode.with_modes print_modes (fn () => cmd print_ctxt) () end;
+ in [Print_Mode.with_modes print_modes (fn () => command src print_ctxt) ()] end;
in
-fun evaluate _ (Antiquote.Text ss) = Symbol_Pos.content ss
- | evaluate ctxt (Antiquote.Control {name, body, ...}) =
+fun evaluate ctxt antiq =
+ (case antiq of
+ Antiquote.Text ss => [Latex.symbols ss]
+ | Antiquote.Control {name, body, ...} =>
eval ctxt ([], Token.make_src name (if null body then [] else [Token.read_cartouche body]))
- | evaluate ctxt (Antiquote.Antiq {range = (pos, _), body, ...}) =
+ | Antiquote.Antiq {range = (pos, _), body, ...} =>
let val keywords = Thy_Header.get_keywords' ctxt;
- in eval ctxt (Token.read_antiq keywords antiq (body, pos)) end;
+ in eval ctxt (Token.read_antiq keywords parse_antiq (body, pos)) end);
end;
@@ -153,13 +184,13 @@
fun boolean "" = true
| boolean "true" = true
| boolean "false" = false
- | boolean s = error ("Bad boolean value: " ^ quote s);
+ | boolean s = error ("Bad boolean value: " ^ Library.quote s);
fun integer s =
let
fun int ss =
(case Library.read_int ss of (i, []) => i
- | _ => error ("Bad integer value: " ^ quote s));
+ | _ => error ("Bad integer value: " ^ Library.quote s));
in (case Symbol.explode s of "-" :: ss => ~ (int ss) | ss => int ss) end;
val _ = Theory.setup
@@ -175,7 +206,7 @@
setup_option \<^binding>\<open>display\<close> (Config.put thy_output_display o boolean) #>
setup_option \<^binding>\<open>break\<close> (Config.put thy_output_break o boolean) #>
setup_option \<^binding>\<open>quotes\<close> (Config.put thy_output_quotes o boolean) #>
- setup_option \<^binding>\<open>mode\<close> (add_wrapper o Print_Mode.with_modes o single) #>
+ setup_option \<^binding>\<open>mode\<close> (Config.put thy_output_modes) #>
setup_option \<^binding>\<open>margin\<close> (Config.put thy_output_margin o integer) #>
setup_option \<^binding>\<open>indent\<close> (Config.put thy_output_indent o integer) #>
setup_option \<^binding>\<open>source\<close> (Config.put thy_output_source o boolean) #>
--- a/src/Pure/Thy/document_antiquotations.ML Fri Jan 19 15:50:17 2018 +0100
+++ b/src/Pure/Thy/document_antiquotations.ML Fri Jan 19 20:11:14 2018 +0100
@@ -11,17 +11,19 @@
local
-fun pretty_term_style ctxt (style, t: term) =
+type style = term -> term;
+
+fun pretty_term_style ctxt (style: style, t) =
Thy_Output.pretty_term ctxt (style t);
-fun pretty_thm_style ctxt (style, th) =
+fun pretty_thm_style ctxt (style: style, th) =
Thy_Output.pretty_term ctxt (style (Thm.full_prop_of th));
-fun pretty_term_typ ctxt (style, t: term) =
+fun pretty_term_typ ctxt (style: style, t) =
let val t' = style t
in Thy_Output.pretty_term ctxt (Type.constraint (Term.fastype_of t') t') end;
-fun pretty_term_typeof ctxt (style, t) =
+fun pretty_term_typeof ctxt (style: style, t) =
Syntax.pretty_typ ctxt (Term.fastype_of (style t));
fun pretty_const ctxt c =
@@ -61,15 +63,11 @@
fun pretty_theory ctxt (name, pos) = (Theory.check ctxt (name, pos); Pretty.str name);
fun basic_entities name scan pretty =
- Document_Antiquotation.setup name scan (fn {source, context = ctxt, ...} =>
- Thy_Output.output ctxt o Thy_Output.maybe_pretty_source pretty ctxt source);
+ Thy_Output.antiquotation_pretty_source name scan (map o pretty);
fun basic_entities_style name scan pretty =
- Document_Antiquotation.setup name scan
- (fn {source, context = ctxt, ...} => fn (style, xs) =>
- Thy_Output.output ctxt
- (Thy_Output.maybe_pretty_source
- (fn ctxt => fn x => pretty ctxt (style, x)) ctxt source xs));
+ Thy_Output.antiquotation_pretty_source name scan
+ (fn ctxt => fn (style: style, xs) => map (fn x => pretty ctxt (style, x)) xs);
fun basic_entity name scan = basic_entities name (scan >> single);
@@ -100,9 +98,9 @@
fun markdown_error binding =
Document_Antiquotation.setup binding (Scan.succeed ())
- (fn {source, ...} => fn _ =>
+ (fn {source = src, ...} =>
error ("Bad Markdown structure: illegal " ^ quote (Binding.name_of binding) ^
- Position.here (Position.no_range_position (#1 (Token.range_of source)))))
+ Position.here (Position.no_range_position (#1 (Token.range_of src)))))
in
@@ -119,14 +117,14 @@
val _ =
Theory.setup
- (Document_Antiquotation.setup \<^binding>\<open>noindent\<close> (Scan.succeed ())
- (K (K "\\noindent")) #>
- Document_Antiquotation.setup \<^binding>\<open>smallskip\<close> (Scan.succeed ())
- (K (K "\\smallskip")) #>
- Document_Antiquotation.setup \<^binding>\<open>medskip\<close> (Scan.succeed ())
- (K (K "\\medskip")) #>
- Document_Antiquotation.setup \<^binding>\<open>bigskip\<close> (Scan.succeed ())
- (K (K "\\bigskip")));
+ (Thy_Output.antiquotation_raw \<^binding>\<open>noindent\<close> (Scan.succeed ())
+ (fn _ => fn () => Latex.string "\\noindent") #>
+ Thy_Output.antiquotation_raw \<^binding>\<open>smallskip\<close> (Scan.succeed ())
+ (fn _ => fn () => Latex.string "\\smallskip") #>
+ Thy_Output.antiquotation_raw \<^binding>\<open>medskip\<close> (Scan.succeed ())
+ (fn _ => fn () => Latex.string "\\medskip") #>
+ Thy_Output.antiquotation_raw \<^binding>\<open>bigskip\<close> (Scan.succeed ())
+ (fn _ => fn () => Latex.string "\\bigskip"));
(* control style *)
@@ -134,9 +132,8 @@
local
fun control_antiquotation name s1 s2 =
- Document_Antiquotation.setup name (Scan.lift Args.cartouche_input)
- (fn {context = ctxt, ...} =>
- enclose s1 s2 o Latex.output_text o Thy_Output.output_text ctxt {markdown = false});
+ Thy_Output.antiquotation_raw name (Scan.lift Args.cartouche_input)
+ (fn ctxt => Latex.enclose_block s1 s2 o Thy_Output.output_text ctxt {markdown = false});
in
@@ -153,62 +150,65 @@
local
+fun report_text ctxt text =
+ Context_Position.report ctxt (Input.pos_of text)
+ (Markup.language_text (Input.is_delimited text));
+
+fun prepare_text ctxt =
+ Input.source_content #> Document_Antiquotation.prepare_lines ctxt;
+
fun text_antiquotation name =
- Document_Antiquotation.setup 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)]));
+ Thy_Output.antiquotation_raw name (Scan.lift Args.text_input)
+ (fn ctxt => fn text =>
+ let
+ val _ = report_text ctxt text;
+ in
+ prepare_text ctxt text
+ |> Thy_Output.output_source ctxt
+ |> Thy_Output.isabelle ctxt
+ end);
+
+val theory_text_antiquotation =
+ Thy_Output.antiquotation_raw \<^binding>\<open>theory_text\<close> (Scan.lift Args.text_input)
+ (fn ctxt => fn text =>
+ let
+ val keywords = Thy_Header.get_keywords' ctxt;
+
+ val _ = report_text ctxt text;
+ val _ =
+ Input.source_explode text
+ |> Source.of_list
+ |> Token.source' true keywords
+ |> Source.exhaust
+ |> maps (Token.reports keywords)
+ |> Context_Position.reports_text ctxt;
+ in
+ prepare_text ctxt text
+ |> Token.explode keywords Position.none
+ |> maps (Thy_Output.output_token ctxt)
+ |> Thy_Output.isabelle ctxt
+ end);
in
val _ =
Theory.setup
(text_antiquotation \<^binding>\<open>text\<close> #>
- text_antiquotation \<^binding>\<open>cartouche\<close>);
+ text_antiquotation \<^binding>\<open>cartouche\<close> #>
+ theory_text_antiquotation);
end;
-(* theory text with tokens (unchecked) *)
-
-val _ =
- Theory.setup
- (Document_Antiquotation.setup \<^binding>\<open>theory_text\<close> (Scan.lift Args.text_input)
- (fn {context = ctxt, ...} => fn source =>
- let
- val _ =
- Context_Position.report ctxt (Input.pos_of source)
- (Markup.language_Isar (Input.is_delimited source));
-
- val keywords = Thy_Header.get_keywords' ctxt;
- val toks =
- Input.source_explode source
- |> not (Config.get ctxt Document_Antiquotation.thy_output_display) ?
- Symbol_Pos.trim_lines
- |> Source.of_list
- |> Token.source' true keywords
- |> Source.exhaust;
- val _ = Context_Position.reports_text ctxt (maps (Token.reports keywords) toks);
- val indentation =
- Latex.output_symbols
- (replicate (Config.get ctxt Document_Antiquotation.thy_output_indent) Symbol.space);
- in
- Latex.output_text (maps (Thy_Output.output_token ctxt) toks) |>
- (if Config.get ctxt Document_Antiquotation.thy_output_display then
- split_lines #> map (prefix indentation) #> cat_lines #>
- Latex.environment "isabelle"
- else enclose "\\isa{" "}")
- end));
(* goal state *)
local
-fun goal_state name main = Document_Antiquotation.setup name (Scan.succeed ())
- (fn {context = ctxt, ...} => fn () =>
- Thy_Output.output ctxt
+fun goal_state name main =
+ Thy_Output.antiquotation_pretty name (Scan.succeed ())
+ (fn ctxt => fn () =>
[Goal_Display.pretty_goal
(Config.put Goal_Display.show_main_goal main ctxt)
(#goal (Proof.goal (Toplevel.proof_of (Toplevel.presentation_state ctxt))))]);
@@ -228,7 +228,7 @@
(Document_Antiquotation.setup \<^binding>\<open>lemma\<close>
(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)) =>
+ (fn {context = ctxt, source = src, argument = ((prop_tok, prop), (((_, by_pos), m1), m2))} =>
let
val reports =
(by_pos, Markup.keyword1 |> Markup.keyword_properties) ::
@@ -239,32 +239,30 @@
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 [hd source, prop_token] [prop])
- end));
+ in Thy_Output.pretty_source ctxt [hd src, prop_tok] [Thy_Output.pretty_term ctxt prop] end));
(* verbatim text *)
-val _ =
- Theory.setup
- (Document_Antiquotation.setup \<^binding>\<open>verbatim\<close> (Scan.lift Args.text_input)
- (fn {context = ctxt, ...} => fn source =>
- (Context_Position.report ctxt (Input.pos_of source)
- (Markup.language_verbatim (Input.is_delimited source));
- Thy_Output.verbatim_text ctxt (Input.source_content source))));
+val _ = Theory.setup
+ (Thy_Output.antiquotation_verbatim \<^binding>\<open>verbatim\<close> (Scan.lift Args.text_input)
+ (fn ctxt => fn text =>
+ let
+ val _ =
+ Context_Position.report ctxt (Input.pos_of text)
+ (Markup.language_verbatim (Input.is_delimited text));
+ in Input.source_content text end));
(* ML text *)
local
-fun ml_text name ml = Document_Antiquotation.setup 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_text name ml =
+ Thy_Output.antiquotation_verbatim name (Scan.lift Args.text_input)
+ (fn ctxt => fn text =>
+ let val _ = ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (Input.pos_of text) (ml text)
+ in Input.source_content text end);
fun ml_enclose bg en source =
ML_Lex.read bg @ ML_Lex.read_source false source @ ML_Lex.read en;
@@ -291,34 +289,30 @@
(* URLs *)
val _ = Theory.setup
- (Document_Antiquotation.setup \<^binding>\<open>url\<close> (Scan.lift (Parse.position Parse.embedded))
- (fn {context = ctxt, ...} => fn (name, pos) =>
- (Context_Position.reports ctxt [(pos, Markup.language_path), (pos, Markup.url name)];
- enclose "\\url{" "}" name)));
-
-
-(* doc entries *)
-
-val _ = Theory.setup
- (Document_Antiquotation.setup \<^binding>\<open>doc\<close> (Scan.lift (Parse.position Parse.embedded))
- (fn {context = ctxt, ...} => fn (name, pos) =>
- (Context_Position.report ctxt pos (Markup.doc name);
- Thy_Output.output ctxt [Thy_Output.pretty_text ctxt name])));
+ (Thy_Output.antiquotation_raw \<^binding>\<open>url\<close> (Scan.lift (Parse.position Parse.embedded))
+ (fn ctxt => fn (url, pos) =>
+ let val _ = Context_Position.reports ctxt [(pos, Markup.language_path), (pos, Markup.url url)]
+ in Latex.enclose_block "\\url{" "}" [Latex.string url] end));
(* formal entities *)
-fun entity_antiquotation name check output =
- Document_Antiquotation.setup name (Scan.lift (Parse.position Args.name))
- (fn {context = ctxt, ...} => fn (name, pos) => (check ctxt (name, pos); output name));
+local
+
+fun entity_antiquotation name check bg en =
+ Thy_Output.antiquotation_raw name (Scan.lift (Parse.position Args.name))
+ (fn ctxt => fn (name, pos) =>
+ let val _ = check ctxt (name, pos)
+ in Latex.enclose_block bg en [Latex.string (Output.output name)] end);
+
+in
val _ =
Theory.setup
- (entity_antiquotation \<^binding>\<open>command\<close> Outer_Syntax.check_command
- (enclose "\\isacommand{" "}" o Output.output) #>
- entity_antiquotation \<^binding>\<open>method\<close> Method.check_name
- (enclose "\\isa{" "}" o Output.output) #>
- entity_antiquotation \<^binding>\<open>attribute\<close> Attrib.check_name
- (enclose "\\isa{" "}" o Output.output));
+ (entity_antiquotation \<^binding>\<open>command\<close> Outer_Syntax.check_command "\\isacommand{" "}" #>
+ entity_antiquotation \<^binding>\<open>method\<close> Method.check_name "\\isa{" "}" #>
+ entity_antiquotation \<^binding>\<open>attribute\<close> Attrib.check_name "\\isa{" "}");
end;
+
+end;
--- a/src/Pure/Thy/latex.ML Fri Jan 19 15:50:17 2018 +0100
+++ b/src/Pure/Thy/latex.ML Fri Jan 19 20:11:14 2018 +0100
@@ -11,12 +11,15 @@
val text: string * Position.T -> text
val block: text list -> text
val enclose_body: string -> string -> text list -> text list
+ val enclose_block: string -> string -> text list -> text
val output_text: text list -> string
val output_positions: Position.T -> text list -> string
val output_name: string -> string
val output_ascii: string -> string
val output_symbols: Symbol.symbol list -> string
val output_syms: string -> string
+ val symbols: Symbol_Pos.T list -> text
+ val symbols_output: Symbol_Pos.T list -> text
val begin_delim: string -> string
val end_delim: string -> string
val begin_tag: string -> string
@@ -76,6 +79,8 @@
(if bg = "" then [] else [string bg]) @ body @
(if en = "" then [] else [string en]);
+fun enclose_block bg en = block o enclose_body bg en;
+
(* output name for LaTeX macros *)
@@ -198,6 +203,10 @@
end;
+fun symbols syms = text (Symbol_Pos.content syms, #1 (Symbol_Pos.range syms));
+fun symbols_output syms =
+ text (output_symbols (map Symbol_Pos.symbol syms), #1 (Symbol_Pos.range syms));
+
(* tags *)
--- a/src/Pure/Thy/markdown.ML Fri Jan 19 15:50:17 2018 +0100
+++ b/src/Pure/Thy/markdown.ML Fri Jan 19 20:11:14 2018 +0100
@@ -132,8 +132,8 @@
fun block_source (Par lines) = maps line_source lines
| block_source (List {body, ...}) = maps line_source (maps block_lines body);
-fun block_range (Par lines) = Antiquote.range (maps line_content lines)
- | block_range (List {body, ...}) = Antiquote.range (maps line_source (maps block_lines body));
+fun block_range (Par lines) = Antiquote.text_range (maps line_content lines)
+ | block_range (List {body, ...}) = Antiquote.text_range (maps line_source (maps block_lines body));
fun block_indent (List {indent, ...}) = indent
| block_indent (Par (Line {indent, ...} :: _)) = indent
@@ -204,7 +204,7 @@
local
val block_pos = #1 o block_range;
-val item_pos = #1 o Antiquote.range o maps block_source;
+val item_pos = #1 o Antiquote.text_range o maps block_source;
fun line_reports depth (Line {bullet_pos, content, ...}) =
cons (bullet_pos, Markup.markdown_bullet depth) #> append (text_reports content);
--- a/src/Pure/Thy/sessions.scala Fri Jan 19 15:50:17 2018 +0100
+++ b/src/Pure/Thy/sessions.scala Fri Jan 19 20:11:14 2018 +0100
@@ -129,6 +129,7 @@
sealed case class Base(
pos: Position.T = Position.none,
+ doc_names: List[String] = Nil,
global_theories: Map[String, String] = Map.empty,
loaded_theories: Graph[String, Outer_Syntax] = Graph.string,
known: Known = Known.empty,
@@ -221,6 +222,8 @@
}
}
+ val doc_names = Doc.doc_names()
+
val session_bases =
(Map.empty[String, Base] /: sessions_structure.imports_topological_order)({
case (session_bases, session_name) =>
@@ -328,6 +331,7 @@
val base =
Base(
pos = info.pos,
+ doc_names = doc_names,
global_theories = global_theories,
loaded_theories = dependencies.loaded_theories,
known = known,
--- a/src/Pure/Thy/thy_output.ML Fri Jan 19 15:50:17 2018 +0100
+++ b/src/Pure/Thy/thy_output.ML Fri Jan 19 20:11:14 2018 +0100
@@ -10,17 +10,27 @@
val check_comments: Proof.context -> Symbol_Pos.T list -> unit
val check_token_comments: Proof.context -> Token.T -> unit
val output_token: Proof.context -> Token.T -> Latex.text list
+ val output_source: Proof.context -> string -> Latex.text list
val present_thy: theory -> (Toplevel.transition * Toplevel.state) list ->
Token.T list -> Latex.text list
- val pretty_text: Proof.context -> string -> Pretty.T
val pretty_term: Proof.context -> term -> Pretty.T
val pretty_thm: Proof.context -> thm -> Pretty.T
- val str_of_source: Token.src -> string
- val maybe_pretty_source: (Proof.context -> 'a -> Pretty.T) -> Proof.context ->
- Token.src -> 'a list -> Pretty.T list
- val string_of_margin: Proof.context -> Pretty.T -> string
- val output: Proof.context -> Pretty.T list -> string
- val verbatim_text: Proof.context -> string -> string
+ val lines: Latex.text list -> Latex.text list
+ val isabelle: Proof.context -> Latex.text list -> Latex.text
+ val isabelle_typewriter: Proof.context -> Latex.text list -> Latex.text
+ val typewriter: Proof.context -> string -> Latex.text
+ val verbatim: Proof.context -> string -> Latex.text
+ val source: Proof.context -> Token.src -> Latex.text
+ val pretty: Proof.context -> Pretty.T list -> Latex.text
+ val pretty_source: Proof.context -> Token.src -> Pretty.T list -> Latex.text
+ val antiquotation_pretty:
+ binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T list) -> theory -> theory
+ val antiquotation_pretty_source:
+ binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T list) -> theory -> theory
+ val antiquotation_raw:
+ binding -> 'a context_parser -> (Proof.context -> 'a -> Latex.text) -> theory -> theory
+ val antiquotation_verbatim:
+ binding -> 'a context_parser -> (Proof.context -> 'a -> string) -> theory -> theory
end;
structure Thy_Output: THY_OUTPUT =
@@ -35,9 +45,7 @@
val _ = Context_Position.report ctxt pos (Markup.language_document (Input.is_delimited source));
- val output_antiquotes =
- map (fn ant =>
- Latex.text (Document_Antiquotation.evaluate ctxt ant, #1 (Antiquote.range [ant])));
+ val output_antiquotes = maps (Document_Antiquotation.evaluate ctxt);
fun output_line line =
(if Markdown.line_is_item line then [Latex.string "\\item "] else []) @
@@ -60,7 +68,7 @@
in output_blocks blocks end
else
let
- val ants = Antiquote.parse pos (Symbol_Pos.trim_blanks syms);
+ val ants = Antiquote.parse pos (trim (Symbol.is_blank o Symbol_Pos.symbol) syms);
val reports = Antiquote.antiq_reports ants;
val _ = Context_Position.reports ctxt (reports @ Markdown.text_reports ants);
in output_antiquotes ants end
@@ -71,11 +79,7 @@
local
-fun output_latex syms =
- [Latex.text (Symbol_Pos.content syms, #1 (Symbol_Pos.range syms))];
-
-fun output_symbols syms =
- [Latex.text (Latex.output_symbols (map Symbol_Pos.symbol syms), #1 (Symbol_Pos.range syms))];
+val output_symbols = single o Latex.symbols_output;
val output_symbols_antiq =
(fn Antiquote.Text syms => output_symbols syms
@@ -95,15 +99,17 @@
let
val body = Symbol_Pos.cartouche_content syms;
val source = Input.source true (Symbol_Pos.implode body) (Symbol_Pos.range body);
+ val ctxt' = ctxt
+ |> Config.put Document_Antiquotation.thy_output_display false;
in
- output_text ctxt {markdown = false} source
+ output_text ctxt' {markdown = false} source
|> Latex.enclose_body "%\n\\isamarkupcmt{" "%\n}"
end
| (SOME Comment.Cancel, _) =>
output_symbols (Symbol_Pos.cartouche_content syms)
|> Latex.enclose_body "%\n\\isamarkupcancel{" "}"
| (SOME Comment.Latex, _) =>
- output_latex (Symbol_Pos.cartouche_content syms));
+ [Latex.symbols (Symbol_Pos.cartouche_content syms)]);
in
@@ -130,6 +136,9 @@
| _ => output false "" "")
end handle ERROR msg => error (msg ^ Position.here (Token.pos_of tok));
+fun output_source ctxt s =
+ output_body ctxt false "" "" (Symbol_Pos.explode (s, Position.none));
+
fun check_comments ctxt =
Comment.read_body #> (Option.app o List.app) (fn (comment, syms) =>
let
@@ -425,58 +434,66 @@
(** standard output operations **)
-(* basic pretty printing *)
-
-fun perhaps_trim ctxt =
- not (Config.get ctxt Document_Antiquotation.thy_output_display) ? Symbol.trim_blanks;
+(* pretty printing *)
-fun pretty_text ctxt =
- Pretty.chunks o map Pretty.str o map (perhaps_trim ctxt) o split_lines;
-
-fun pretty_term ctxt t = Syntax.pretty_term (Variable.auto_fixes t ctxt) t;
+fun pretty_term ctxt t =
+ Syntax.pretty_term (Variable.auto_fixes t ctxt) t;
fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of;
(* default output *)
-val str_of_source = space_implode " " o map Token.unparse o Token.args_of_src;
+val lines = separate (Latex.string "\\isasep\\isanewline%\n");
+
+fun isabelle ctxt body =
+ if Config.get ctxt Document_Antiquotation.thy_output_display
+ then Latex.environment_block "isabelle" body
+ else Latex.block (Latex.enclose_body "\\isa{" "}" body);
-fun maybe_pretty_source pretty ctxt src xs =
- map (pretty ctxt) xs (*always pretty in order to exhibit errors!*)
- |> (if Config.get ctxt Document_Antiquotation.thy_output_source
- then K [pretty_text ctxt (str_of_source src)] else I);
+fun isabelle_typewriter ctxt body =
+ if Config.get ctxt Document_Antiquotation.thy_output_display
+ then Latex.environment_block "isabellett" body
+ else Latex.block (Latex.enclose_body "\\isatt{" "}" body);
-fun string_of_margin ctxt =
- Pretty.string_of_margin (Config.get ctxt Document_Antiquotation.thy_output_margin);
+fun typewriter ctxt s =
+ isabelle_typewriter ctxt [Latex.string (Latex.output_ascii s)];
-fun output ctxt prts =
- prts
- |> Config.get ctxt Document_Antiquotation.thy_output_quotes ? map Pretty.quote
- |> (if Config.get ctxt Document_Antiquotation.thy_output_display then
- map (Pretty.indent (Config.get ctxt Document_Antiquotation.thy_output_indent)
- #> string_of_margin ctxt #> Output.output)
- #> space_implode "\\isasep\\isanewline%\n"
- #> Latex.environment "isabelle"
- else
- map
- ((if Config.get ctxt Document_Antiquotation.thy_output_break
- then string_of_margin ctxt else Pretty.unformatted_string_of) #> Output.output)
- #> space_implode "\\isasep\\isanewline%\n"
- #> enclose "\\isa{" "}");
+fun verbatim ctxt =
+ if Config.get ctxt Document_Antiquotation.thy_output_display
+ then Document_Antiquotation.indent_lines ctxt #> typewriter ctxt
+ else split_lines #> map (typewriter ctxt) #> lines #> Latex.block;
+
+fun source ctxt =
+ Token.args_of_src
+ #> map (Token.unparse #> Document_Antiquotation.prepare_lines ctxt)
+ #> space_implode " "
+ #> output_source ctxt
+ #> isabelle ctxt;
+
+fun pretty ctxt =
+ map (Document_Antiquotation.output ctxt #> Latex.string) #> lines #> isabelle ctxt;
+
+fun pretty_source ctxt src prts =
+ if Config.get ctxt Document_Antiquotation.thy_output_source
+ then source ctxt src else pretty ctxt prts;
-(* verbatim text *)
+(* antiquotation variants *)
+
+fun antiquotation_pretty name scan f =
+ Document_Antiquotation.setup name scan
+ (fn {context = ctxt, argument = x, ...} => pretty ctxt (f ctxt x));
-fun verbatim_text ctxt =
- if Config.get ctxt Document_Antiquotation.thy_output_display then
- split_lines #>
- map (prefix (Symbol.spaces (Config.get ctxt Document_Antiquotation.thy_output_indent))) #>
- cat_lines #>
- Latex.output_ascii #> Latex.environment "isabellett"
- else
- split_lines #>
- map (Latex.output_ascii #> enclose "\\isatt{" "}") #>
- space_implode "\\isasep\\isanewline%\n";
+fun antiquotation_pretty_source name scan f =
+ Document_Antiquotation.setup name scan
+ (fn {context = ctxt, source = src, argument = x} => pretty_source ctxt src (f ctxt x));
+
+fun antiquotation_raw name scan f =
+ Document_Antiquotation.setup name scan
+ (fn {context = ctxt, argument = x, ...} => f ctxt x);
+
+fun antiquotation_verbatim name scan f =
+ antiquotation_raw name scan (fn ctxt => verbatim ctxt o f ctxt);
end;
--- a/src/Pure/Tools/build.ML Fri Jan 19 15:50:17 2018 +0100
+++ b/src/Pure/Tools/build.ML Fri Jan 19 20:11:14 2018 +0100
@@ -150,6 +150,7 @@
master_dir: Path.T,
theories: (Options.T * (string * Position.T) list) list,
sessions: string list,
+ doc_names: string list,
global_theories: (string * string) list,
loaded_theories: string list,
known_theories: (string * string) list,
@@ -161,14 +162,14 @@
val position = Position.of_properties o properties;
val (symbol_codes, (command_timings, (do_output, (verbose, (browser_info,
(document_files, (graph_file, (parent_name, (chapter, (name, (master_dir,
- (theories, (sessions, (global_theories, (loaded_theories,
- (known_theories, bibtex_entries)))))))))))))))) =
+ (theories, (sessions, (doc_names, (global_theories, (loaded_theories,
+ (known_theories, bibtex_entries))))))))))))))))) =
pair (list (pair string int)) (pair (list properties) (pair bool (pair bool (pair string
(pair (list (pair string string)) (pair string (pair string (pair string (pair string
(pair string
(pair (((list (pair Options.decode (list (pair string position))))))
- (pair (list string) (pair (list (pair string string)) (pair (list string)
- (pair (list (pair string string)) (list string))))))))))))))))
+ (pair (list string) (pair (list string) (pair (list (pair string string)) (pair (list string)
+ (pair (list (pair string string)) (list string)))))))))))))))))
(YXML.parse_body yxml);
in
Args {symbol_codes = symbol_codes, command_timings = command_timings, do_output = do_output,
@@ -176,19 +177,20 @@
document_files = map (apply2 Path.explode) document_files,
graph_file = Path.explode graph_file, parent_name = parent_name, chapter = chapter,
name = name, master_dir = Path.explode master_dir, theories = theories, sessions = sessions,
- global_theories = global_theories, loaded_theories = loaded_theories,
+ doc_names = doc_names, global_theories = global_theories, loaded_theories = loaded_theories,
known_theories = known_theories, bibtex_entries = bibtex_entries}
end;
fun build_session (Args {symbol_codes, command_timings, do_output, verbose, browser_info,
document_files, graph_file, parent_name, chapter, name, master_dir, theories, sessions,
- global_theories, loaded_theories, known_theories, bibtex_entries}) =
+ doc_names, global_theories, loaded_theories, known_theories, bibtex_entries}) =
let
val symbols = HTML.make_symbols symbol_codes;
val _ =
Resources.init_session_base
{sessions = sessions,
+ doc_names = doc_names,
global_theories = global_theories,
loaded_theories = loaded_theories,
known_theories = known_theories};
--- a/src/Pure/Tools/build.scala Fri Jan 19 15:50:17 2018 +0100
+++ b/src/Pure/Tools/build.scala Fri Jan 19 20:11:14 2018 +0100
@@ -212,16 +212,14 @@
pair(Path.encode, pair(list(pair(Path.encode, Path.encode)), pair(string,
pair(string, pair(string, pair(string, pair(Path.encode,
pair(list(pair(Options.encode, list(pair(string, properties)))),
- pair(list(string), pair(list(pair(string, string)), pair(list(string),
- pair(list(pair(string, string)), list(string)))))))))))))))))(
+ pair(list(string), pair(list(string), pair(list(pair(string, string)),
+ pair(list(string), pair(list(pair(string, string)), list(string))))))))))))))))))(
(Symbol.codes, (command_timings, (do_output, (verbose,
(store.browser_info, (info.document_files, (File.standard_path(graph_file),
(parent, (info.chapter, (name, (Path.current,
- (info.theories, (base.known.sessions.toList,
- (base.global_theories.toList,
- (base.loaded_theories.keys,
- (base.dest_known_theories,
- info.bibtex_entries.map(_.info))))))))))))))))))
+ (info.theories, (base.known.sessions.toList, (base.doc_names,
+ (base.global_theories.toList, (base.loaded_theories.keys, (base.dest_known_theories,
+ info.bibtex_entries.map(_.info)))))))))))))))))))
})
val env =
--- a/src/Pure/Tools/doc.scala Fri Jan 19 15:50:17 2018 +0100
+++ b/src/Pure/Tools/doc.scala Fri Jan 19 20:11:14 2018 +0100
@@ -77,6 +77,9 @@
examples() ::: release_notes() ::: main_contents
}
+ def doc_names(): List[String] =
+ for (Doc(name, _, _) <- contents()) yield name
+
/* view */
--- a/src/Pure/Tools/jedit.ML Fri Jan 19 15:50:17 2018 +0100
+++ b/src/Pure/Tools/jedit.ML Fri Jan 19 20:11:14 2018 +0100
@@ -75,10 +75,14 @@
val _ =
Theory.setup
- (Document_Antiquotation.setup \<^binding>\<open>action\<close> (Scan.lift (Parse.position Parse.embedded))
- (fn {context = ctxt, ...} => fn (name, pos) =>
- (if Context_Position.is_reported ctxt pos then ignore (check_action (name, pos)) else ();
- Thy_Output.verbatim_text ctxt name)));
+ (Thy_Output.antiquotation_verbatim \<^binding>\<open>action\<close> (Scan.lift (Parse.position Parse.embedded))
+ (fn ctxt => fn (name, pos) =>
+ let
+ val _ =
+ if Context_Position.is_reported ctxt pos
+ then ignore (check_action (name, pos))
+ else ();
+ in name end));
end;
--- a/src/Pure/Tools/rail.ML Fri Jan 19 15:50:17 2018 +0100
+++ b/src/Pure/Tools/rail.ML Fri Jan 19 20:11:14 2018 +0100
@@ -17,7 +17,7 @@
Terminal of bool * string |
Antiquote of bool * Antiquote.antiq
val read: Proof.context -> Input.source -> (string Antiquote.antiquote * rail) list
- val output_rules: Proof.context -> (string Antiquote.antiquote * rail) list -> string
+ val output_rules: Proof.context -> (string Antiquote.antiquote * rail) list -> Latex.text
end;
structure Rail: RAIL =
@@ -339,7 +339,8 @@
fun output_rules ctxt rules =
let
- val output_antiq = Document_Antiquotation.evaluate ctxt o Antiquote.Antiq;
+ val output_antiq =
+ Latex.output_text o Document_Antiquotation.evaluate ctxt o Antiquote.Antiq;
fun output_text b s =
Output.output s
|> b ? enclose "\\isakeyword{" "}"
@@ -378,11 +379,11 @@
output "" rail' ^
"\\rail@end\n"
end;
- in Latex.environment "railoutput" (implode (map output_rule rules)) end;
+ in Latex.string (Latex.environment "railoutput" (implode (map output_rule rules))) end;
val _ = Theory.setup
- (Document_Antiquotation.setup \<^binding>\<open>rail\<close> (Scan.lift Args.text_input)
- (fn {context = ctxt, ...} => output_rules ctxt o read ctxt));
+ (Thy_Output.antiquotation_raw \<^binding>\<open>rail\<close> (Scan.lift Args.text_input)
+ (fn ctxt => output_rules ctxt o read ctxt));
end;
--- a/src/Tools/Code/code_target.ML Fri Jan 19 15:50:17 2018 +0100
+++ b/src/Tools/Code/code_target.ML Fri Jan 19 20:11:14 2018 +0100
@@ -510,14 +510,15 @@
in
val _ = Theory.setup
- (Document_Antiquotation.setup @{binding code_stmts}
+ (Thy_Output.antiquotation_raw @{binding code_stmts}
(parse_const_terms --
Scan.repeat (parse_consts || parse_types || parse_classes || parse_instances)
-- Scan.lift (Args.parens (Args.name -- Scan.option Parse.int)))
- (fn {context = ctxt, ...} => fn ((mk_cs, mk_stmtss), (target_name, some_width)) =>
- present_code ctxt (mk_cs ctxt)
+ (fn ctxt => fn ((mk_cs, mk_stmtss), (target_name, some_width)) =>
+ Latex.string
+ (present_code ctxt (mk_cs ctxt)
(maps (fn f => f ctxt) mk_stmtss)
- target_name some_width "Example" []));
+ target_name some_width "Example" [])));
end;