merged default tip
authorwenzelm
Fri Jan 19 20:11:14 2018 +0100 (18 hours ago)
changeset 67477056be95db703
parent 67459 7264dfad077c
parent 67476 44b018d4aa5f
merged
     1.1 --- a/etc/symbols	Fri Jan 19 15:50:17 2018 +0100
     1.2 +++ b/etc/symbols	Fri Jan 19 20:11:14 2018 +0100
     1.3 @@ -410,6 +410,7 @@
     1.4  \<^plugin>              argument: cartouche
     1.5  \<^print>
     1.6  \<^prop>                argument: cartouche
     1.7 +\<^session>             argument: cartouche
     1.8  \<^simproc>             argument: cartouche
     1.9  \<^sort>                argument: cartouche
    1.10  \<^syntax_const>        argument: cartouche
     2.1 --- a/src/Doc/Isar_Ref/Outer_Syntax.thy	Fri Jan 19 15:50:17 2018 +0100
     2.2 +++ b/src/Doc/Isar_Ref/Outer_Syntax.thy	Fri Jan 19 20:11:14 2018 +0100
     2.3 @@ -255,8 +255,8 @@
     2.4    document preparation (\chref{ch:document-prep}) supports various styles,
     2.5    according to the following kinds of comments.
     2.6  
     2.7 -    \<^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
     2.8 -    single space between the comment symbol and the argument cartouche. The
     2.9 +    \<^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
    2.10 +    a single space between the comment symbol and the argument cartouche. The
    2.11      given argument is typeset as regular text, with formal antiquotations
    2.12      (\secref{sec:antiq}).
    2.13  
     3.1 --- a/src/Doc/Main/Main_Doc.thy	Fri Jan 19 15:50:17 2018 +0100
     3.2 +++ b/src/Doc/Main/Main_Doc.thy	Fri Jan 19 20:11:14 2018 +0100
     3.3 @@ -4,23 +4,15 @@
     3.4  begin
     3.5  
     3.6  setup \<open>
     3.7 -  let
     3.8 -    fun pretty_term_type_only ctxt (t, T) =
     3.9 +  Thy_Output.antiquotation_pretty_source @{binding term_type_only} (Args.term -- Args.typ_abbrev)
    3.10 +    (fn ctxt => fn (t, T) =>
    3.11        (if fastype_of t = Sign.certify_typ (Proof_Context.theory_of ctxt) T then ()
    3.12         else error "term_type_only: type mismatch";
    3.13 -       Syntax.pretty_typ ctxt T)
    3.14 -  in
    3.15 -    Document_Antiquotation.setup @{binding term_type_only}
    3.16 -      (Args.term -- Args.typ_abbrev)
    3.17 -      (fn {source, context = ctxt, ...} => fn arg =>
    3.18 -        Thy_Output.output ctxt
    3.19 -          (Thy_Output.maybe_pretty_source pretty_term_type_only ctxt source [arg]))
    3.20 -  end
    3.21 +       [Syntax.pretty_typ ctxt T]))
    3.22  \<close>
    3.23  setup \<open>
    3.24 -  Document_Antiquotation.setup @{binding expanded_typ} (Args.typ >> single)
    3.25 -    (fn {source, context, ...} => Thy_Output.output context o
    3.26 -      Thy_Output.maybe_pretty_source Syntax.pretty_typ context source)
    3.27 +  Thy_Output.antiquotation_pretty_source @{binding expanded_typ} Args.typ
    3.28 +    (fn ctxt => fn T => [Syntax.pretty_typ ctxt T])
    3.29  \<close>
    3.30  (*>*)
    3.31  text\<open>
     4.1 --- a/src/Doc/Prog_Prove/LaTeXsugar.thy	Fri Jan 19 15:50:17 2018 +0100
     4.2 +++ b/src/Doc/Prog_Prove/LaTeXsugar.thy	Fri Jan 19 20:11:14 2018 +0100
     4.3 @@ -43,20 +43,13 @@
     4.4    "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^latex>\<open>{\\normalsize \\,\<close>and\<^latex>\<open>\\,}\<close>/ _")
     4.5    "_asm" :: "prop \<Rightarrow> asms" ("_")
     4.6  
     4.7 -setup\<open>
     4.8 -  let
     4.9 -    fun pretty ctxt c =
    4.10 -      let val tc = Proof_Context.read_const {proper = true, strict = false} ctxt c
    4.11 -      in Pretty.block [Thy_Output.pretty_term ctxt tc, Pretty.str " ::",
    4.12 -            Pretty.brk 1, Syntax.pretty_typ ctxt (fastype_of tc)]
    4.13 -      end
    4.14 -  in
    4.15 -    Document_Antiquotation.setup @{binding "const_typ"}
    4.16 -     (Scan.lift Args.embedded_inner_syntax)
    4.17 -       (fn {source = src, context = ctxt, ...} => fn arg =>
    4.18 -          Thy_Output.output ctxt
    4.19 -            (Thy_Output.maybe_pretty_source pretty ctxt src [arg]))
    4.20 -  end;
    4.21 +setup \<open>
    4.22 +  Thy_Output.antiquotation_pretty_source \<^binding>\<open>const_typ\<close> (Scan.lift Args.embedded_inner_syntax)
    4.23 +    (fn ctxt => fn c =>
    4.24 +      let val tc = Proof_Context.read_const {proper = true, strict = false} ctxt c in
    4.25 +        [Pretty.block [Thy_Output.pretty_term ctxt tc, Pretty.str " ::",
    4.26 +          Pretty.brk 1, Syntax.pretty_typ ctxt (fastype_of tc)]]
    4.27 +      end)
    4.28  \<close>
    4.29  
    4.30  end
     5.1 --- a/src/Doc/antiquote_setup.ML	Fri Jan 19 15:50:17 2018 +0100
     5.2 +++ b/src/Doc/antiquote_setup.ML	Fri Jan 19 20:11:14 2018 +0100
     5.3 @@ -73,9 +73,9 @@
     5.4  fun prep_ml source =
     5.5    (Input.source_content source, ML_Lex.read_source false source);
     5.6  
     5.7 -fun index_ml name kind ml = Document_Antiquotation.setup name
     5.8 +fun index_ml name kind ml = Thy_Output.antiquotation_raw name
     5.9    (Scan.lift (Args.text_input -- Scan.option (Args.colon |-- Args.text_input)))
    5.10 -  (fn {context = ctxt, ...} => fn (source1, opt_source2) =>
    5.11 +  (fn ctxt => fn (source1, opt_source2) =>
    5.12      let
    5.13        val (txt1, toks1) = prep_ml source1;
    5.14        val (txt2, toks2) =
    5.15 @@ -98,8 +98,9 @@
    5.16            handle ERROR msg => error (msg ^ Position.here pos);
    5.17        val kind' = if kind = "" then "ML" else "ML " ^ kind;
    5.18      in
    5.19 -      "\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string (ml_name txt1) ^ "}" ^
    5.20 -      (Thy_Output.verbatim_text ctxt txt')
    5.21 +      Latex.block
    5.22 +       [Latex.string ("\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string (ml_name txt1) ^ "}"),
    5.23 +        Thy_Output.verbatim ctxt txt']
    5.24      end);
    5.25  
    5.26  in
    5.27 @@ -119,29 +120,17 @@
    5.28  (* named theorems *)
    5.29  
    5.30  val _ =
    5.31 -  Theory.setup (Document_Antiquotation.setup @{binding named_thms}
    5.32 +  Theory.setup (Thy_Output.antiquotation_raw @{binding named_thms}
    5.33      (Scan.repeat (Attrib.thm -- Scan.lift (Args.parens Args.name)))
    5.34 -    (fn {context = ctxt, ...} =>
    5.35 -      map (apfst (Thy_Output.pretty_thm ctxt))
    5.36 -      #> (if Config.get ctxt Document_Antiquotation.thy_output_quotes
    5.37 -          then map (apfst Pretty.quote) else I)
    5.38 -      #> (if Config.get ctxt Document_Antiquotation.thy_output_display
    5.39 -          then
    5.40 -            map (fn (p, name) =>
    5.41 -              Output.output
    5.42 -                (Thy_Output.string_of_margin ctxt
    5.43 -                  (Pretty.indent (Config.get ctxt Document_Antiquotation.thy_output_indent) p)) ^
    5.44 -              "\\rulename{" ^
    5.45 -              Output.output (Pretty.unformatted_string_of (Thy_Output.pretty_text ctxt name)) ^ "}")
    5.46 -            #> space_implode "\\par\\smallskip%\n"
    5.47 -            #> Latex.environment "isabelle"
    5.48 -          else
    5.49 -            map (fn (p, name) =>
    5.50 -              Output.output (Pretty.unformatted_string_of p) ^
    5.51 -              "\\rulename{" ^
    5.52 -              Output.output (Pretty.unformatted_string_of (Thy_Output.pretty_text ctxt name)) ^ "}")
    5.53 -            #> space_implode "\\par\\smallskip%\n"
    5.54 -            #> enclose "\\isa{" "}")));
    5.55 +    (fn ctxt =>
    5.56 +      map (fn (thm, name) =>
    5.57 +        Output.output
    5.58 +          (Document_Antiquotation.format ctxt
    5.59 +            (Document_Antiquotation.quote ctxt (Thy_Output.pretty_thm ctxt thm))) ^
    5.60 +        enclose "\\rulename{" "}" (Output.output name))
    5.61 +      #> space_implode "\\par\\smallskip%\n"
    5.62 +      #> Latex.string #> single
    5.63 +      #> Thy_Output.isabelle ctxt));
    5.64  
    5.65  
    5.66  (* Isabelle/Isar entities (with index) *)
    5.67 @@ -161,11 +150,11 @@
    5.68  val arg = enclose "{" "}" o clean_string;
    5.69  
    5.70  fun entity check markup binding index =
    5.71 -  Document_Antiquotation.setup
    5.72 +  Thy_Output.antiquotation_raw
    5.73      (binding |> Binding.map_name (fn name => name ^
    5.74        (case index of NONE => "" | SOME true => "_def" | SOME false => "_ref")))
    5.75      (Scan.lift (Scan.optional (Args.parens Args.name) "" -- Parse.position Args.name))
    5.76 -    (fn {context = ctxt, ...} => fn (logic, (name, pos)) =>
    5.77 +    (fn ctxt => fn (logic, (name, pos)) =>
    5.78        let
    5.79          val kind = translate (fn "_" => " " | c => c) (Binding.name_of binding);
    5.80          val hyper_name =
    5.81 @@ -180,12 +169,12 @@
    5.82                "\\index" ^ (if is_def then "def" else "ref") ^ arg logic ^ arg kind ^ arg name);
    5.83          val _ =
    5.84            if Context_Position.is_reported ctxt pos then ignore (check ctxt (name, pos)) else ();
    5.85 -      in
    5.86 -        idx ^
    5.87 -        (Output.output name
    5.88 -          |> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}")
    5.89 -          |> hyper o enclose "\\mbox{\\isa{" "}}")
    5.90 -      end);
    5.91 +        val latex =
    5.92 +          idx ^
    5.93 +          (Output.output name
    5.94 +            |> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}")
    5.95 +            |> hyper o enclose "\\mbox{\\isa{" "}}");
    5.96 +      in Latex.string latex end);
    5.97  
    5.98  fun entity_antiqs check markup kind =
    5.99    entity check markup kind NONE #>
     6.1 --- a/src/Doc/more_antiquote.ML	Fri Jan 19 15:50:17 2018 +0100
     6.2 +++ b/src/Doc/more_antiquote.ML	Fri Jan 19 20:11:14 2018 +0100
     6.3 @@ -9,53 +9,37 @@
     6.4  
     6.5  (* class specifications *)
     6.6  
     6.7 -local
     6.8 -
     6.9 -fun class_spec ctxt s =
    6.10 -  let
    6.11 -    val thy = Proof_Context.theory_of ctxt;
    6.12 -    val class = Sign.intern_class thy s;
    6.13 -  in Thy_Output.output ctxt (Class.pretty_specification thy class) end;
    6.14 -
    6.15 -in
    6.16 -
    6.17  val _ =
    6.18 -  Theory.setup (Document_Antiquotation.setup @{binding class_spec} (Scan.lift Args.name)
    6.19 -    (fn {context, ...} => class_spec context));
    6.20 -
    6.21 -end;
    6.22 +  Theory.setup (Thy_Output.antiquotation_pretty @{binding class_spec} (Scan.lift Args.name)
    6.23 +    (fn ctxt => fn s =>
    6.24 +      let
    6.25 +        val thy = Proof_Context.theory_of ctxt;
    6.26 +        val class = Sign.intern_class thy s;
    6.27 +      in Class.pretty_specification thy class end));
    6.28  
    6.29  
    6.30  (* code theorem antiquotation *)
    6.31  
    6.32 -local
    6.33 -
    6.34  fun no_vars ctxt thm =
    6.35    let
    6.36      val ctxt' = Variable.set_body false ctxt;
    6.37      val ((_, [thm]), _) = Variable.import true [thm] ctxt';
    6.38    in thm end;
    6.39  
    6.40 -fun pretty_code_thm ctxt raw_const =
    6.41 -  let
    6.42 -    val thy = Proof_Context.theory_of ctxt;
    6.43 -    val const = Code.check_const thy raw_const;
    6.44 -    val { eqngr, ... } = Code_Preproc.obtain true { ctxt = ctxt, consts = [const], terms = [] };
    6.45 -    fun holize thm = @{thm meta_eq_to_obj_eq} OF [thm];
    6.46 -    val thms = Code_Preproc.cert eqngr const
    6.47 -      |> Code.equations_of_cert thy
    6.48 -      |> snd
    6.49 -      |> these
    6.50 -      |> map_filter (fn (_, (some_thm, proper)) => if proper then some_thm else NONE)
    6.51 -      |> map (holize o no_vars ctxt o Axclass.overload ctxt);
    6.52 -  in Thy_Output.output ctxt (map (Thy_Output.pretty_thm ctxt) thms) end;
    6.53 -
    6.54 -in
    6.55 -
    6.56  val _ =
    6.57 -  Theory.setup (Document_Antiquotation.setup @{binding code_thms} Args.term
    6.58 -    (fn {context, ...} => pretty_code_thm context));
    6.59 +  Theory.setup (Thy_Output.antiquotation_pretty @{binding code_thms} Args.term
    6.60 +    (fn ctxt => fn raw_const =>
    6.61 +      let
    6.62 +        val thy = Proof_Context.theory_of ctxt;
    6.63 +        val const = Code.check_const thy raw_const;
    6.64 +        val { eqngr, ... } = Code_Preproc.obtain true { ctxt = ctxt, consts = [const], terms = [] };
    6.65 +        fun holize thm = @{thm meta_eq_to_obj_eq} OF [thm];
    6.66 +        val thms = Code_Preproc.cert eqngr const
    6.67 +          |> Code.equations_of_cert thy
    6.68 +          |> snd
    6.69 +          |> these
    6.70 +          |> map_filter (fn (_, (some_thm, proper)) => if proper then some_thm else NONE)
    6.71 +          |> map (holize o no_vars ctxt o Axclass.overload ctxt);
    6.72 +      in map (Thy_Output.pretty_thm ctxt) thms end));
    6.73  
    6.74  end;
    6.75 -
    6.76 -end;
     7.1 --- a/src/HOL/Library/LaTeXsugar.thy	Fri Jan 19 15:50:17 2018 +0100
     7.2 +++ b/src/HOL/Library/LaTeXsugar.thy	Fri Jan 19 20:11:14 2018 +0100
     7.3 @@ -96,20 +96,13 @@
     7.4    "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^latex>\<open>{\\normalsize \\,\<close>and\<^latex>\<open>\\,}\<close>/ _")
     7.5    "_asm" :: "prop \<Rightarrow> asms" ("_")
     7.6  
     7.7 -setup\<open>
     7.8 -  let
     7.9 -    fun pretty ctxt c =
    7.10 -      let val tc = Proof_Context.read_const {proper = true, strict = false} ctxt c
    7.11 -      in Pretty.block [Thy_Output.pretty_term ctxt tc, Pretty.str " ::",
    7.12 -            Pretty.brk 1, Syntax.pretty_typ ctxt (fastype_of tc)]
    7.13 -      end
    7.14 -  in
    7.15 -    Document_Antiquotation.setup @{binding "const_typ"}
    7.16 -     (Scan.lift Args.embedded_inner_syntax)
    7.17 -       (fn {source = src, context = ctxt, ...} => fn arg =>
    7.18 -          Thy_Output.output ctxt
    7.19 -            (Thy_Output.maybe_pretty_source pretty ctxt src [arg]))
    7.20 -  end;
    7.21 +setup \<open>
    7.22 +  Thy_Output.antiquotation_pretty_source \<^binding>\<open>const_typ\<close> (Scan.lift Args.embedded_inner_syntax)
    7.23 +    (fn ctxt => fn c =>
    7.24 +      let val tc = Proof_Context.read_const {proper = true, strict = false} ctxt c in
    7.25 +        [Pretty.block [Thy_Output.pretty_term ctxt tc, Pretty.str " ::",
    7.26 +          Pretty.brk 1, Syntax.pretty_typ ctxt (fastype_of tc)]]
    7.27 +      end)
    7.28  \<close>
    7.29  
    7.30  setup\<open>
     8.1 --- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Fri Jan 19 15:50:17 2018 +0100
     8.2 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Fri Jan 19 20:11:14 2018 +0100
     8.3 @@ -983,8 +983,8 @@
     8.4    end;
     8.5  
     8.6  fun fp_antiquote_setup binding =
     8.7 -  Document_Antiquotation.setup binding (Args.type_name {proper = true, strict = true})
     8.8 -    (fn {source = src, context = ctxt, ...} => fn fcT_name =>
     8.9 +  Thy_Output.antiquotation_pretty_source binding (Args.type_name {proper = true, strict = true})
    8.10 +    (fn ctxt => fn fcT_name =>
    8.11         (case Ctr_Sugar.ctr_sugar_of ctxt fcT_name of
    8.12           NONE => error ("Not a known freely generated type name: " ^ quote fcT_name)
    8.13         | SOME {T = T0, ctrs = ctrs0, ...} =>
    8.14 @@ -1002,9 +1002,6 @@
    8.15               Pretty.block (Pretty.keyword1 (Binding.name_of binding) :: Pretty.brk 1 ::
    8.16                 Syntax.pretty_typ ctxt T :: Pretty.str " =" :: Pretty.brk 1 ::
    8.17                 flat (separate [Pretty.brk 1, Pretty.str "| "] (map (single o pretty_ctr) ctrs)));
    8.18 -         in
    8.19 -           Thy_Output.output ctxt
    8.20 -             (Thy_Output.maybe_pretty_source (K (K pretty_co_datatype)) ctxt src [()])
    8.21 -         end));
    8.22 +         in [pretty_co_datatype] end));
    8.23  
    8.24  end;
     9.1 --- a/src/HOL/Tools/value_command.ML	Fri Jan 19 15:50:17 2018 +0100
     9.2 +++ b/src/HOL/Tools/value_command.ML	Fri Jan 19 20:11:14 2018 +0100
     9.3 @@ -73,11 +73,10 @@
     9.4        >> (fn ((name, modes), t) => Toplevel.keep (value_cmd name modes t)));
     9.5  
     9.6  val _ = Theory.setup
     9.7 -  (Document_Antiquotation.setup \<^binding>\<open>value\<close>
     9.8 +  (Thy_Output.antiquotation_pretty_source \<^binding>\<open>value\<close>
     9.9      (Scan.lift opt_evaluator -- Term_Style.parse -- Args.term)
    9.10 -    (fn {source, context, ...} => fn ((name, style), t) => Thy_Output.output context
    9.11 -      (Thy_Output.maybe_pretty_source Thy_Output.pretty_term context source
    9.12 -        [style (value_select name context t)]))
    9.13 +    (fn ctxt => fn ((name, style), t) =>
    9.14 +      [Thy_Output.pretty_term ctxt (style (value_select name ctxt t))])
    9.15    #> add_evaluator (\<^binding>\<open>simp\<close>, Code_Simp.dynamic_value) #> snd
    9.16    #> add_evaluator (\<^binding>\<open>nbe\<close>, Nbe.dynamic_value) #> snd
    9.17    #> add_evaluator (\<^binding>\<open>code\<close>, Code_Evaluation.dynamic_value_strict) #> snd);
    10.1 --- a/src/Pure/General/antiquote.ML	Fri Jan 19 15:50:17 2018 +0100
    10.2 +++ b/src/Pure/General/antiquote.ML	Fri Jan 19 20:11:14 2018 +0100
    10.3 @@ -10,7 +10,8 @@
    10.4    type antiq = {start: Position.T, stop: Position.T, range: Position.range, body: Symbol_Pos.T list}
    10.5    datatype 'a antiquote = Text of 'a | Control of control | Antiq of antiq
    10.6    type text_antiquote = Symbol_Pos.T list antiquote
    10.7 -  val range: text_antiquote list -> Position.range
    10.8 +  val text_antiquote_range: text_antiquote -> Position.range
    10.9 +  val text_range: text_antiquote list -> Position.range
   10.10    val split_lines: text_antiquote list -> text_antiquote list list
   10.11    val antiq_reports: 'a antiquote list -> Position.report list
   10.12    val scan_control: control scanner
   10.13 @@ -31,13 +32,14 @@
   10.14  
   10.15  type text_antiquote = Symbol_Pos.T list antiquote;
   10.16  
   10.17 -fun antiquote_range (Text ss) = Symbol_Pos.range ss
   10.18 -  | antiquote_range (Control {range, ...}) = range
   10.19 -  | antiquote_range (Antiq {range, ...}) = range;
   10.20 +fun text_antiquote_range (Text ss) = Symbol_Pos.range ss
   10.21 +  | text_antiquote_range (Control {range, ...}) = range
   10.22 +  | text_antiquote_range (Antiq {range, ...}) = range;
   10.23  
   10.24 -fun range ants =
   10.25 +fun text_range ants =
   10.26    if null ants then Position.no_range
   10.27 -  else Position.range (#1 (antiquote_range (hd ants)), #2 (antiquote_range (List.last ants)));
   10.28 +  else
   10.29 +    Position.range (#1 (text_antiquote_range (hd ants)), #2 (text_antiquote_range (List.last ants)));
   10.30  
   10.31  
   10.32  (* split lines *)
    11.1 --- a/src/Pure/General/symbol_pos.ML	Fri Jan 19 15:50:17 2018 +0100
    11.2 +++ b/src/Pure/General/symbol_pos.ML	Fri Jan 19 20:11:14 2018 +0100
    11.3 @@ -11,9 +11,6 @@
    11.4    val symbol: T -> Symbol.symbol
    11.5    val content: T list -> string
    11.6    val range: T list -> Position.range
    11.7 -  val split_lines: T list -> T list list
    11.8 -  val trim_blanks: T list -> T list
    11.9 -  val trim_lines: T list -> T list
   11.10    val is_eof: T -> bool
   11.11    val stopper: T Scan.stopper
   11.12    val !!! : Scan.message -> 'a scanner -> 'a scanner
   11.13 @@ -69,23 +66,6 @@
   11.14    | range [] = Position.no_range;
   11.15  
   11.16  
   11.17 -(* lines and blanks *)
   11.18 -
   11.19 -fun split_lines [] = []
   11.20 -  | split_lines (list: T list) =
   11.21 -      let
   11.22 -        fun split syms =
   11.23 -          (case take_prefix (fn (s, _) => s <> "\n") syms of
   11.24 -            (line, []) => [line]
   11.25 -          | (line, _ :: rest) => line :: split rest);
   11.26 -      in split list end;
   11.27 -
   11.28 -val trim_blanks = trim (Symbol.is_blank o symbol);
   11.29 -
   11.30 -val trim_lines =
   11.31 -  split_lines #> map trim_blanks #> separate [(Symbol.space, Position.none)] #> flat;
   11.32 -
   11.33 -
   11.34  (* stopper *)
   11.35  
   11.36  fun mk_eof pos = (Symbol.eof, pos);
    12.1 --- a/src/Pure/ML/ml_process.scala	Fri Jan 19 15:50:17 2018 +0100
    12.2 +++ b/src/Pure/ML/ml_process.scala	Fri Jan 19 20:11:14 2018 +0100
    12.3 @@ -103,6 +103,7 @@
    12.4              ML_Syntax.print_list(ML_Syntax.print_string_bytes)(list)
    12.5            List("Resources.init_session_base" +
    12.6              " {sessions = " + print_list(base.known.sessions.toList) +
    12.7 +            ", doc_names = " + print_list(base.doc_names) +
    12.8              ", global_theories = " + print_table(base.global_theories.toList) +
    12.9              ", loaded_theories = " + print_list(base.loaded_theories.keys) +
   12.10              ", known_theories = " + print_table(base.dest_known_theories) + "}")
    13.1 --- a/src/Pure/PIDE/protocol.ML	Fri Jan 19 15:50:17 2018 +0100
    13.2 +++ b/src/Pure/PIDE/protocol.ML	Fri Jan 19 20:11:14 2018 +0100
    13.3 @@ -19,13 +19,15 @@
    13.4  
    13.5  val _ =
    13.6    Isabelle_Process.protocol_command "Prover.init_session_base"
    13.7 -    (fn [sessions_yxml, global_theories_yxml, loaded_theories_yxml, known_theories_yxml] =>
    13.8 +    (fn [sessions_yxml, doc_names_yxml, global_theories_yxml, loaded_theories_yxml,
    13.9 +          known_theories_yxml] =>
   13.10        let
   13.11          val decode_table = YXML.parse_body #> let open XML.Decode in list (pair string string) end;
   13.12          val decode_list = YXML.parse_body #> let open XML.Decode in list string end;
   13.13        in
   13.14          Resources.init_session_base
   13.15            {sessions = decode_list sessions_yxml,
   13.16 +           doc_names = decode_list doc_names_yxml,
   13.17             global_theories = decode_table global_theories_yxml,
   13.18             loaded_theories = decode_list loaded_theories_yxml,
   13.19             known_theories = decode_table known_theories_yxml}
    14.1 --- a/src/Pure/PIDE/protocol.scala	Fri Jan 19 15:50:17 2018 +0100
    14.2 +++ b/src/Pure/PIDE/protocol.scala	Fri Jan 19 20:11:14 2018 +0100
    14.3 @@ -343,6 +343,7 @@
    14.4      val base = resources.session_base.standard_path
    14.5      protocol_command("Prover.init_session_base",
    14.6        encode_list(base.known.sessions.toList),
    14.7 +      encode_list(base.doc_names),
    14.8        encode_table(base.global_theories.toList),
    14.9        encode_list(base.loaded_theories.keys),
   14.10        encode_table(base.dest_known_theories))
    15.1 --- a/src/Pure/PIDE/resources.ML	Fri Jan 19 15:50:17 2018 +0100
    15.2 +++ b/src/Pure/PIDE/resources.ML	Fri Jan 19 20:11:14 2018 +0100
    15.3 @@ -9,6 +9,7 @@
    15.4    val default_qualifier: string
    15.5    val init_session_base:
    15.6      {sessions: string list,
    15.7 +     doc_names: string list,
    15.8       global_theories: (string * string) list,
    15.9       loaded_theories: string list,
   15.10       known_theories: (string * string) list} -> unit
   15.11 @@ -17,6 +18,7 @@
   15.12    val loaded_theory: string -> bool
   15.13    val known_theory: string -> Path.T option
   15.14    val check_session: Proof.context -> string * Position.T -> string
   15.15 +  val check_doc: Proof.context -> string * Position.T -> string
   15.16    val master_directory: theory -> Path.T
   15.17    val imports_of: theory -> (string * Position.T) list
   15.18    val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory
   15.19 @@ -45,6 +47,7 @@
   15.20  
   15.21  val empty_session_base =
   15.22    {sessions = []: string list,
   15.23 +   doc_names = []: string list,
   15.24     global_theories = Symtab.empty: string Symtab.table,
   15.25     loaded_theories = Symtab.empty: unit Symtab.table,
   15.26     known_theories = Symtab.empty: Path.T Symtab.table};
   15.27 @@ -52,10 +55,11 @@
   15.28  val global_session_base =
   15.29    Synchronized.var "Sessions.base" empty_session_base;
   15.30  
   15.31 -fun init_session_base {sessions, global_theories, loaded_theories, known_theories} =
   15.32 +fun init_session_base {sessions, doc_names, global_theories, loaded_theories, known_theories} =
   15.33    Synchronized.change global_session_base
   15.34      (fn _ =>
   15.35        {sessions = sort_strings sessions,
   15.36 +       doc_names = doc_names,
   15.37         global_theories = Symtab.make global_theories,
   15.38         loaded_theories = Symtab.make_set loaded_theories,
   15.39         known_theories = Symtab.make (map (apsnd Path.explode) known_theories)});
   15.40 @@ -64,6 +68,7 @@
   15.41    Synchronized.change global_session_base
   15.42      (fn {global_theories, loaded_theories, ...} =>
   15.43        {sessions = [],
   15.44 +       doc_names = [],
   15.45         global_theories = global_theories,
   15.46         loaded_theories = loaded_theories,
   15.47         known_theories = #known_theories empty_session_base});
   15.48 @@ -74,21 +79,26 @@
   15.49  fun loaded_theory a = Symtab.defined (get_session_base #loaded_theories) a;
   15.50  fun known_theory a = Symtab.lookup (get_session_base #known_theories) a;
   15.51  
   15.52 -fun check_session ctxt (name, pos) =
   15.53 -  let val sessions = get_session_base #sessions in
   15.54 -    if member (op =) sessions name then
   15.55 -      (Context_Position.report ctxt pos (Markup.entity Markup.sessionN name); name)
   15.56 +fun check_name which kind markup ctxt (name, pos) =
   15.57 +  let val names = get_session_base which in
   15.58 +    if member (op =) names name then
   15.59 +      (Context_Position.report ctxt pos (markup name); name)
   15.60      else
   15.61        let
   15.62          val completion =
   15.63            Completion.make (name, pos) (fn completed =>
   15.64 -              sessions
   15.65 +              names
   15.66                |> filter completed
   15.67 -              |> map (fn a => (a, (Markup.sessionN, a))));
   15.68 +              |> sort_strings
   15.69 +              |> map (fn a => (a, (kind, a))));
   15.70          val report = Markup.markup_report (Completion.reported_text completion);
   15.71 -      in error ("Bad session " ^ quote name ^ Position.here pos ^ report) end
   15.72 +      in error ("Bad " ^ kind ^ " " ^ quote name ^ Position.here pos ^ report) end
   15.73    end;
   15.74  
   15.75 +val check_session = check_name #sessions "session" (Markup.entity Markup.sessionN);
   15.76 +val check_doc = check_name #doc_names "documentation" Markup.doc;
   15.77 +
   15.78 +
   15.79  
   15.80  (* manage source files *)
   15.81  
   15.82 @@ -243,12 +253,11 @@
   15.83    let
   15.84      val dir = master_directory (Proof_Context.theory_of ctxt);
   15.85      val _ = check ctxt dir (name, pos);
   15.86 -  in
   15.87 -    space_explode "/" name
   15.88 -    |> map Latex.output_ascii
   15.89 -    |> space_implode (Latex.output_ascii "/" ^ "\\discretionary{}{}{}")
   15.90 -    |> enclose "\\isatt{" "}"
   15.91 -  end;
   15.92 +    val latex =
   15.93 +      space_explode "/" name
   15.94 +      |> map Latex.output_ascii
   15.95 +      |> space_implode (Latex.output_ascii "/" ^ "\\discretionary{}{}{}");
   15.96 +  in Latex.enclose_block "\\isatt{" "}" [Latex.string latex] end;
   15.97  
   15.98  fun ML_antiq check ctxt (name, pos) =
   15.99    let val path = check ctxt Path.current (name, pos);
  15.100 @@ -257,14 +266,16 @@
  15.101  in
  15.102  
  15.103  val _ = Theory.setup
  15.104 - (Document_Antiquotation.setup \<^binding>\<open>session\<close> (Scan.lift (Parse.position Parse.embedded))
  15.105 -    (fn {context = ctxt, ...} => Thy_Output.verbatim_text ctxt o check_session ctxt) #>
  15.106 -  Document_Antiquotation.setup \<^binding>\<open>path\<close> (Scan.lift (Parse.position Parse.path))
  15.107 -    (document_antiq check_path o #context) #>
  15.108 -  Document_Antiquotation.setup \<^binding>\<open>file\<close> (Scan.lift (Parse.position Parse.path))
  15.109 -    (document_antiq check_file o #context) #>
  15.110 -  Document_Antiquotation.setup \<^binding>\<open>dir\<close> (Scan.lift (Parse.position Parse.path))
  15.111 -    (document_antiq check_dir o #context) #>
  15.112 + (Thy_Output.antiquotation_verbatim \<^binding>\<open>session\<close>
  15.113 +    (Scan.lift (Parse.position Parse.embedded)) check_session #>
  15.114 +  Thy_Output.antiquotation_verbatim \<^binding>\<open>doc\<close>
  15.115 +    (Scan.lift (Parse.position Parse.embedded)) check_doc #>
  15.116 +  Thy_Output.antiquotation_raw \<^binding>\<open>path\<close>
  15.117 +    (Scan.lift (Parse.position Parse.path)) (document_antiq check_path) #>
  15.118 +  Thy_Output.antiquotation_raw \<^binding>\<open>file\<close>
  15.119 +    (Scan.lift (Parse.position Parse.path)) (document_antiq check_file) #>
  15.120 +  Thy_Output.antiquotation_raw \<^binding>\<open>dir\<close>
  15.121 +    (Scan.lift (Parse.position Parse.path)) (document_antiq check_dir) #>
  15.122    ML_Antiquotation.value \<^binding>\<open>path\<close>
  15.123      (Args.context -- Scan.lift (Parse.position Parse.path) >> uncurry (ML_antiq check_path)) #>
  15.124    ML_Antiquotation.value \<^binding>\<open>file\<close>
    16.1 --- a/src/Pure/Thy/bibtex.ML	Fri Jan 19 15:50:17 2018 +0100
    16.2 +++ b/src/Pure/Thy/bibtex.ML	Fri Jan 19 20:11:14 2018 +0100
    16.3 @@ -41,11 +41,11 @@
    16.4  val _ =
    16.5    Theory.setup
    16.6     (Document_Antiquotation.setup_option \<^binding>\<open>cite_macro\<close> (Config.put cite_macro) #>
    16.7 -    Document_Antiquotation.setup \<^binding>\<open>cite\<close>
    16.8 +    Thy_Output.antiquotation_raw \<^binding>\<open>cite\<close>
    16.9        (Scan.lift
   16.10          (Scan.option (Parse.verbatim || Parse.cartouche) --
   16.11           Parse.and_list1 (Parse.position Args.name)))
   16.12 -      (fn {context = ctxt, ...} => fn (opt, citations) =>
   16.13 +      (fn ctxt => fn (opt, citations) =>
   16.14          let
   16.15            val thy = Proof_Context.theory_of ctxt;
   16.16            val bibtex_entries = Present.get_bibtex_entries thy;
   16.17 @@ -60,6 +60,6 @@
   16.18                (map (fn (name, pos) => (pos, Markup.citation name)) citations);
   16.19            val opt_arg = (case opt of NONE => "" | SOME s => "[" ^ s ^ "]");
   16.20            val arg = "{" ^ space_implode "," (map #1 citations) ^ "}";
   16.21 -        in "\\" ^ Config.get ctxt cite_macro ^ opt_arg ^ arg end));
   16.22 +        in Latex.string ("\\" ^ Config.get ctxt cite_macro ^ opt_arg ^ arg) end));
   16.23  
   16.24  end;
    17.1 --- a/src/Pure/Thy/document_antiquotation.ML	Fri Jan 19 15:50:17 2018 +0100
    17.2 +++ b/src/Pure/Thy/document_antiquotation.ML	Fri Jan 19 20:11:14 2018 +0100
    17.3 @@ -13,16 +13,23 @@
    17.4    val thy_output_source: bool Config.T
    17.5    val thy_output_break: bool Config.T
    17.6    val thy_output_modes: string Config.T
    17.7 -  val add_wrapper: ((unit -> string) -> unit -> string) -> Proof.context -> Proof.context
    17.8 +  val trim_blanks: Proof.context -> string -> string
    17.9 +  val trim_lines: Proof.context -> string -> string
   17.10 +  val indent_lines: Proof.context -> string -> string
   17.11 +  val prepare_lines: Proof.context -> string -> string
   17.12 +  val quote: Proof.context -> Pretty.T -> Pretty.T
   17.13 +  val indent: Proof.context -> Pretty.T -> Pretty.T
   17.14 +  val format: Proof.context -> Pretty.T -> string
   17.15 +  val output: Proof.context -> Pretty.T -> Output.output
   17.16    val print_antiquotations: bool -> Proof.context -> unit
   17.17    val check: Proof.context -> xstring * Position.T -> string
   17.18    val check_option: Proof.context -> xstring * Position.T -> string
   17.19    val setup: binding -> 'a context_parser ->
   17.20 -    ({source: Token.src, context: Proof.context} -> 'a -> string) -> theory -> theory
   17.21 +    ({context: Proof.context, source: Token.src, argument: 'a} -> Latex.text) -> theory -> theory
   17.22    val setup_option: binding -> (string -> Proof.context -> Proof.context) -> theory -> theory
   17.23    val boolean: string -> bool
   17.24    val integer: string -> int
   17.25 -  val evaluate: Proof.context -> Antiquote.text_antiquote -> string
   17.26 +  val evaluate: Proof.context -> Antiquote.text_antiquote -> Latex.text list
   17.27  end;
   17.28  
   17.29  structure Document_Antiquotation: DOCUMENT_ANTIQUOTATION =
   17.30 @@ -39,15 +46,38 @@
   17.31  val thy_output_modes = Attrib.setup_option_string ("thy_output_modes", \<^here>);
   17.32  
   17.33  
   17.34 -structure Wrappers = Proof_Data
   17.35 -(
   17.36 -  type T = ((unit -> string) -> unit -> string) list;
   17.37 -  fun init _ = [];
   17.38 -);
   17.39 +(* blanks *)
   17.40  
   17.41 -fun add_wrapper wrapper = Wrappers.map (cons wrapper);
   17.42 +fun trim_blanks ctxt =
   17.43 +  not (Config.get ctxt thy_output_display) ? Symbol.trim_blanks;
   17.44  
   17.45 -val wrap = Wrappers.get #> fold (fn wrapper => fn f => wrapper f);
   17.46 +fun trim_lines ctxt =
   17.47 +  if not (Config.get ctxt thy_output_display) then
   17.48 +    split_lines #> map Symbol.trim_blanks #> space_implode " "
   17.49 +  else I;
   17.50 +
   17.51 +fun indent_lines ctxt =
   17.52 +  if Config.get ctxt thy_output_display then
   17.53 +    prefix_lines (Symbol.spaces (Config.get ctxt thy_output_indent))
   17.54 +  else I;
   17.55 +
   17.56 +fun prepare_lines ctxt = trim_lines ctxt #> indent_lines ctxt;
   17.57 +
   17.58 +
   17.59 +(* output *)
   17.60 +
   17.61 +fun quote ctxt =
   17.62 +  Config.get ctxt thy_output_quotes ? Pretty.quote;
   17.63 +
   17.64 +fun indent ctxt =
   17.65 +  Config.get ctxt thy_output_display ? Pretty.indent (Config.get ctxt thy_output_indent);
   17.66 +
   17.67 +fun format ctxt =
   17.68 +  if Config.get ctxt thy_output_display orelse Config.get ctxt thy_output_break
   17.69 +  then Pretty.string_of_margin (Config.get ctxt thy_output_margin)
   17.70 +  else Pretty.unformatted_string_of;
   17.71 +
   17.72 +fun output ctxt = quote ctxt #> indent ctxt #> format ctxt #> Output.output;
   17.73  
   17.74  
   17.75  (* theory data *)
   17.76 @@ -55,7 +85,7 @@
   17.77  structure Data = Theory_Data
   17.78  (
   17.79    type T =
   17.80 -    (Token.src -> Proof.context -> string) Name_Space.table *
   17.81 +    (Token.src -> Proof.context -> Latex.text) Name_Space.table *
   17.82        (string -> Proof.context -> Proof.context) Name_Space.table;
   17.83    val empty : T =
   17.84      (Name_Space.empty_table Markup.document_antiquotationN,
   17.85 @@ -85,7 +115,7 @@
   17.86    let
   17.87      fun cmd src ctxt =
   17.88        let val (x, ctxt') = Token.syntax scan src ctxt
   17.89 -      in body {source = src, context = ctxt'} x end;
   17.90 +      in body {context = ctxt', source = src, argument = x} end;
   17.91    in thy |> Data.map (apfst (Name_Space.define (Context.Theory thy) true (name, cmd) #> #2)) end;
   17.92  
   17.93  fun setup_option name opt thy = thy
   17.94 @@ -104,7 +134,7 @@
   17.95  
   17.96  in
   17.97  
   17.98 -val antiq =
   17.99 +val parse_antiq =
  17.100    Parse.!!!
  17.101      (Parse.token Parse.liberal_name -- properties -- Parse.args --| Scan.ahead Parse.eof)
  17.102    >> (fn ((name, props), args) => (props, name :: args));
  17.103 @@ -129,21 +159,22 @@
  17.104  fun eval ctxt (opts, src) =
  17.105    let
  17.106      val preview_ctxt = fold option opts ctxt;
  17.107 +    val _ = command src preview_ctxt;
  17.108 +
  17.109      val print_ctxt = Context_Position.set_visible false preview_ctxt;
  17.110 -
  17.111 -    fun cmd ctxt = wrap ctxt (fn () => command src ctxt) ();
  17.112 -    val _ = cmd preview_ctxt;
  17.113      val print_modes = space_explode "," (Config.get print_ctxt thy_output_modes) @ [Latex.latexN];
  17.114 -  in Print_Mode.with_modes print_modes (fn () => cmd print_ctxt) () end;
  17.115 +  in [Print_Mode.with_modes print_modes (fn () => command src print_ctxt) ()] end;
  17.116  
  17.117  in
  17.118  
  17.119 -fun evaluate _ (Antiquote.Text ss) = Symbol_Pos.content ss
  17.120 -  | evaluate ctxt (Antiquote.Control {name, body, ...}) =
  17.121 +fun evaluate ctxt antiq =
  17.122 +  (case antiq of
  17.123 +    Antiquote.Text ss => [Latex.symbols ss]
  17.124 +  | Antiquote.Control {name, body, ...} =>
  17.125        eval ctxt ([], Token.make_src name (if null body then [] else [Token.read_cartouche body]))
  17.126 -  | evaluate ctxt (Antiquote.Antiq {range = (pos, _), body, ...}) =
  17.127 +  | Antiquote.Antiq {range = (pos, _), body, ...} =>
  17.128        let val keywords = Thy_Header.get_keywords' ctxt;
  17.129 -      in eval ctxt (Token.read_antiq keywords antiq (body, pos)) end;
  17.130 +      in eval ctxt (Token.read_antiq keywords parse_antiq (body, pos)) end);
  17.131  
  17.132  end;
  17.133  
  17.134 @@ -153,13 +184,13 @@
  17.135  fun boolean "" = true
  17.136    | boolean "true" = true
  17.137    | boolean "false" = false
  17.138 -  | boolean s = error ("Bad boolean value: " ^ quote s);
  17.139 +  | boolean s = error ("Bad boolean value: " ^ Library.quote s);
  17.140  
  17.141  fun integer s =
  17.142    let
  17.143      fun int ss =
  17.144        (case Library.read_int ss of (i, []) => i
  17.145 -      | _ => error ("Bad integer value: " ^ quote s));
  17.146 +      | _ => error ("Bad integer value: " ^ Library.quote s));
  17.147    in (case Symbol.explode s of "-" :: ss => ~ (int ss) | ss => int ss) end;
  17.148  
  17.149  val _ = Theory.setup
  17.150 @@ -175,7 +206,7 @@
  17.151    setup_option \<^binding>\<open>display\<close> (Config.put thy_output_display o boolean) #>
  17.152    setup_option \<^binding>\<open>break\<close> (Config.put thy_output_break o boolean) #>
  17.153    setup_option \<^binding>\<open>quotes\<close> (Config.put thy_output_quotes o boolean) #>
  17.154 -  setup_option \<^binding>\<open>mode\<close> (add_wrapper o Print_Mode.with_modes o single) #>
  17.155 +  setup_option \<^binding>\<open>mode\<close> (Config.put thy_output_modes) #>
  17.156    setup_option \<^binding>\<open>margin\<close> (Config.put thy_output_margin o integer) #>
  17.157    setup_option \<^binding>\<open>indent\<close> (Config.put thy_output_indent o integer) #>
  17.158    setup_option \<^binding>\<open>source\<close> (Config.put thy_output_source o boolean) #>
    18.1 --- a/src/Pure/Thy/document_antiquotations.ML	Fri Jan 19 15:50:17 2018 +0100
    18.2 +++ b/src/Pure/Thy/document_antiquotations.ML	Fri Jan 19 20:11:14 2018 +0100
    18.3 @@ -11,17 +11,19 @@
    18.4  
    18.5  local
    18.6  
    18.7 -fun pretty_term_style ctxt (style, t: term) =
    18.8 +type style = term -> term;
    18.9 +
   18.10 +fun pretty_term_style ctxt (style: style, t) =
   18.11    Thy_Output.pretty_term ctxt (style t);
   18.12  
   18.13 -fun pretty_thm_style ctxt (style, th) =
   18.14 +fun pretty_thm_style ctxt (style: style, th) =
   18.15    Thy_Output.pretty_term ctxt (style (Thm.full_prop_of th));
   18.16  
   18.17 -fun pretty_term_typ ctxt (style, t: term) =
   18.18 +fun pretty_term_typ ctxt (style: style, t) =
   18.19    let val t' = style t
   18.20    in Thy_Output.pretty_term ctxt (Type.constraint (Term.fastype_of t') t') end;
   18.21  
   18.22 -fun pretty_term_typeof ctxt (style, t) =
   18.23 +fun pretty_term_typeof ctxt (style: style, t) =
   18.24    Syntax.pretty_typ ctxt (Term.fastype_of (style t));
   18.25  
   18.26  fun pretty_const ctxt c =
   18.27 @@ -61,15 +63,11 @@
   18.28  fun pretty_theory ctxt (name, pos) = (Theory.check ctxt (name, pos); Pretty.str name);
   18.29  
   18.30  fun basic_entities name scan pretty =
   18.31 -  Document_Antiquotation.setup name scan (fn {source, context = ctxt, ...} =>
   18.32 -    Thy_Output.output ctxt o Thy_Output.maybe_pretty_source pretty ctxt source);
   18.33 +  Thy_Output.antiquotation_pretty_source name scan (map o pretty);
   18.34  
   18.35  fun basic_entities_style name scan pretty =
   18.36 -  Document_Antiquotation.setup name scan
   18.37 -    (fn {source, context = ctxt, ...} => fn (style, xs) =>
   18.38 -      Thy_Output.output ctxt
   18.39 -        (Thy_Output.maybe_pretty_source
   18.40 -          (fn ctxt => fn x => pretty ctxt (style, x)) ctxt source xs));
   18.41 +  Thy_Output.antiquotation_pretty_source name scan
   18.42 +    (fn ctxt => fn (style: style, xs) => map (fn x => pretty ctxt (style, x)) xs);
   18.43  
   18.44  fun basic_entity name scan = basic_entities name (scan >> single);
   18.45  
   18.46 @@ -100,9 +98,9 @@
   18.47  
   18.48  fun markdown_error binding =
   18.49    Document_Antiquotation.setup binding (Scan.succeed ())
   18.50 -    (fn {source, ...} => fn _ =>
   18.51 +    (fn {source = src, ...} =>
   18.52        error ("Bad Markdown structure: illegal " ^ quote (Binding.name_of binding) ^
   18.53 -        Position.here (Position.no_range_position (#1 (Token.range_of source)))))
   18.54 +        Position.here (Position.no_range_position (#1 (Token.range_of src)))))
   18.55  
   18.56  in
   18.57  
   18.58 @@ -119,14 +117,14 @@
   18.59  
   18.60  val _ =
   18.61    Theory.setup
   18.62 -   (Document_Antiquotation.setup \<^binding>\<open>noindent\<close> (Scan.succeed ())
   18.63 -      (K (K "\\noindent")) #>
   18.64 -    Document_Antiquotation.setup \<^binding>\<open>smallskip\<close> (Scan.succeed ())
   18.65 -      (K (K "\\smallskip")) #>
   18.66 -    Document_Antiquotation.setup \<^binding>\<open>medskip\<close> (Scan.succeed ())
   18.67 -      (K (K "\\medskip")) #>
   18.68 -    Document_Antiquotation.setup \<^binding>\<open>bigskip\<close> (Scan.succeed ())
   18.69 -      (K (K "\\bigskip")));
   18.70 +   (Thy_Output.antiquotation_raw \<^binding>\<open>noindent\<close> (Scan.succeed ())
   18.71 +      (fn _ => fn () => Latex.string "\\noindent") #>
   18.72 +    Thy_Output.antiquotation_raw \<^binding>\<open>smallskip\<close> (Scan.succeed ())
   18.73 +      (fn _ => fn () => Latex.string "\\smallskip") #>
   18.74 +    Thy_Output.antiquotation_raw \<^binding>\<open>medskip\<close> (Scan.succeed ())
   18.75 +      (fn _ => fn () => Latex.string "\\medskip") #>
   18.76 +    Thy_Output.antiquotation_raw \<^binding>\<open>bigskip\<close> (Scan.succeed ())
   18.77 +      (fn _ => fn () => Latex.string "\\bigskip"));
   18.78  
   18.79  
   18.80  (* control style *)
   18.81 @@ -134,9 +132,8 @@
   18.82  local
   18.83  
   18.84  fun control_antiquotation name s1 s2 =
   18.85 -  Document_Antiquotation.setup name (Scan.lift Args.cartouche_input)
   18.86 -    (fn {context = ctxt, ...} =>
   18.87 -      enclose s1 s2 o Latex.output_text o Thy_Output.output_text ctxt {markdown = false});
   18.88 +  Thy_Output.antiquotation_raw name (Scan.lift Args.cartouche_input)
   18.89 +    (fn ctxt => Latex.enclose_block s1 s2 o Thy_Output.output_text ctxt {markdown = false});
   18.90  
   18.91  in
   18.92  
   18.93 @@ -153,62 +150,65 @@
   18.94  
   18.95  local
   18.96  
   18.97 +fun report_text ctxt text =
   18.98 +  Context_Position.report ctxt (Input.pos_of text)
   18.99 +    (Markup.language_text (Input.is_delimited text));
  18.100 +
  18.101 +fun prepare_text ctxt =
  18.102 +  Input.source_content #> Document_Antiquotation.prepare_lines ctxt;
  18.103 +
  18.104  fun text_antiquotation name =
  18.105 -  Document_Antiquotation.setup name (Scan.lift Args.text_input)
  18.106 -    (fn {context = ctxt, ...} => fn source =>
  18.107 -     (Context_Position.report ctxt (Input.pos_of source)
  18.108 -        (Markup.language_text (Input.is_delimited source));
  18.109 -      Thy_Output.output ctxt [Thy_Output.pretty_text ctxt (Input.source_content source)]));
  18.110 +  Thy_Output.antiquotation_raw name (Scan.lift Args.text_input)
  18.111 +    (fn ctxt => fn text =>
  18.112 +      let
  18.113 +        val _ = report_text ctxt text;
  18.114 +      in
  18.115 +        prepare_text ctxt text
  18.116 +        |> Thy_Output.output_source ctxt
  18.117 +        |> Thy_Output.isabelle ctxt
  18.118 +      end);
  18.119 +
  18.120 +val theory_text_antiquotation =
  18.121 +  Thy_Output.antiquotation_raw \<^binding>\<open>theory_text\<close> (Scan.lift Args.text_input)
  18.122 +    (fn ctxt => fn text =>
  18.123 +      let
  18.124 +        val keywords = Thy_Header.get_keywords' ctxt;
  18.125 +
  18.126 +        val _ = report_text ctxt text;
  18.127 +        val _ =
  18.128 +          Input.source_explode text
  18.129 +          |> Source.of_list
  18.130 +          |> Token.source' true keywords
  18.131 +          |> Source.exhaust
  18.132 +          |> maps (Token.reports keywords)
  18.133 +          |> Context_Position.reports_text ctxt;
  18.134 +      in
  18.135 +        prepare_text ctxt text
  18.136 +        |> Token.explode keywords Position.none
  18.137 +        |> maps (Thy_Output.output_token ctxt)
  18.138 +        |> Thy_Output.isabelle ctxt
  18.139 +      end);
  18.140  
  18.141  in
  18.142  
  18.143  val _ =
  18.144    Theory.setup
  18.145     (text_antiquotation \<^binding>\<open>text\<close> #>
  18.146 -    text_antiquotation \<^binding>\<open>cartouche\<close>);
  18.147 +    text_antiquotation \<^binding>\<open>cartouche\<close> #>
  18.148 +    theory_text_antiquotation);
  18.149  
  18.150  end;
  18.151  
  18.152  
  18.153 -(* theory text with tokens (unchecked) *)
  18.154 -
  18.155 -val _ =
  18.156 -  Theory.setup
  18.157 -    (Document_Antiquotation.setup \<^binding>\<open>theory_text\<close> (Scan.lift Args.text_input)
  18.158 -      (fn {context = ctxt, ...} => fn source =>
  18.159 -        let
  18.160 -          val _ =
  18.161 -            Context_Position.report ctxt (Input.pos_of source)
  18.162 -              (Markup.language_Isar (Input.is_delimited source));
  18.163 -
  18.164 -          val keywords = Thy_Header.get_keywords' ctxt;
  18.165 -          val toks =
  18.166 -            Input.source_explode source
  18.167 -            |> not (Config.get ctxt Document_Antiquotation.thy_output_display) ?
  18.168 -                Symbol_Pos.trim_lines
  18.169 -            |> Source.of_list
  18.170 -            |> Token.source' true keywords
  18.171 -            |> Source.exhaust;
  18.172 -          val _ = Context_Position.reports_text ctxt (maps (Token.reports keywords) toks);
  18.173 -          val indentation =
  18.174 -            Latex.output_symbols
  18.175 -              (replicate (Config.get ctxt Document_Antiquotation.thy_output_indent) Symbol.space);
  18.176 -        in
  18.177 -          Latex.output_text (maps (Thy_Output.output_token ctxt) toks) |>
  18.178 -           (if Config.get ctxt Document_Antiquotation.thy_output_display then
  18.179 -              split_lines #> map (prefix indentation) #> cat_lines #>
  18.180 -              Latex.environment "isabelle"
  18.181 -            else enclose "\\isa{" "}")
  18.182 -        end));
  18.183  
  18.184  
  18.185  (* goal state *)
  18.186  
  18.187  local
  18.188  
  18.189 -fun goal_state name main = Document_Antiquotation.setup name (Scan.succeed ())
  18.190 -  (fn {context = ctxt, ...} => fn () =>
  18.191 -    Thy_Output.output ctxt
  18.192 +fun goal_state name main =
  18.193 +  Thy_Output.antiquotation_pretty name (Scan.succeed ())
  18.194 +    (fn ctxt => fn () =>
  18.195        [Goal_Display.pretty_goal
  18.196          (Config.put Goal_Display.show_main_goal main ctxt)
  18.197          (#goal (Proof.goal (Toplevel.proof_of (Toplevel.presentation_state ctxt))))]);
  18.198 @@ -228,7 +228,7 @@
  18.199    (Document_Antiquotation.setup \<^binding>\<open>lemma\<close>
  18.200      (Scan.lift (Scan.ahead Parse.not_eof) -- Args.prop --
  18.201        Scan.lift (Parse.position (Parse.reserved "by") -- Method.parse -- Scan.option Method.parse))
  18.202 -    (fn {source, context = ctxt, ...} => fn ((prop_token, prop), (((_, by_pos), m1), m2)) =>
  18.203 +    (fn {context = ctxt, source = src, argument = ((prop_tok, prop), (((_, by_pos), m1), m2))} =>
  18.204        let
  18.205          val reports =
  18.206            (by_pos, Markup.keyword1 |> Markup.keyword_properties) ::
  18.207 @@ -239,32 +239,30 @@
  18.208          val _ = ctxt
  18.209            |> Proof.theorem NONE (K I) [[(prop, [])]]
  18.210            |> Proof.global_terminal_proof (m1, m2);
  18.211 -      in
  18.212 -        Thy_Output.output ctxt
  18.213 -          (Thy_Output.maybe_pretty_source
  18.214 -            Thy_Output.pretty_term ctxt [hd source, prop_token] [prop])
  18.215 -      end));
  18.216 +      in Thy_Output.pretty_source ctxt [hd src, prop_tok] [Thy_Output.pretty_term ctxt prop] end));
  18.217  
  18.218  
  18.219  (* verbatim text *)
  18.220  
  18.221 -val _ =
  18.222 -  Theory.setup
  18.223 -    (Document_Antiquotation.setup \<^binding>\<open>verbatim\<close> (Scan.lift Args.text_input)
  18.224 -      (fn {context = ctxt, ...} => fn source =>
  18.225 -       (Context_Position.report ctxt (Input.pos_of source)
  18.226 -          (Markup.language_verbatim (Input.is_delimited source));
  18.227 -        Thy_Output.verbatim_text ctxt (Input.source_content source))));
  18.228 +val _ = Theory.setup
  18.229 +  (Thy_Output.antiquotation_verbatim \<^binding>\<open>verbatim\<close> (Scan.lift Args.text_input)
  18.230 +    (fn ctxt => fn text =>
  18.231 +      let
  18.232 +        val _ =
  18.233 +          Context_Position.report ctxt (Input.pos_of text)
  18.234 +            (Markup.language_verbatim (Input.is_delimited text));
  18.235 +      in Input.source_content text end));
  18.236  
  18.237  
  18.238  (* ML text *)
  18.239  
  18.240  local
  18.241  
  18.242 -fun ml_text name ml = Document_Antiquotation.setup name (Scan.lift Args.text_input)
  18.243 -  (fn {context = ctxt, ...} => fn source =>
  18.244 -   (ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (Input.pos_of source) (ml source);
  18.245 -    Thy_Output.verbatim_text ctxt (Input.source_content source)));
  18.246 +fun ml_text name ml =
  18.247 +  Thy_Output.antiquotation_verbatim name (Scan.lift Args.text_input)
  18.248 +    (fn ctxt => fn text =>
  18.249 +      let val _ = ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (Input.pos_of text) (ml text)
  18.250 +      in Input.source_content text end);
  18.251  
  18.252  fun ml_enclose bg en source =
  18.253    ML_Lex.read bg @ ML_Lex.read_source false source @ ML_Lex.read en;
  18.254 @@ -291,34 +289,30 @@
  18.255  (* URLs *)
  18.256  
  18.257  val _ = Theory.setup
  18.258 -  (Document_Antiquotation.setup \<^binding>\<open>url\<close> (Scan.lift (Parse.position Parse.embedded))
  18.259 -    (fn {context = ctxt, ...} => fn (name, pos) =>
  18.260 -      (Context_Position.reports ctxt [(pos, Markup.language_path), (pos, Markup.url name)];
  18.261 -       enclose "\\url{" "}" name)));
  18.262 -
  18.263 -
  18.264 -(* doc entries *)
  18.265 -
  18.266 -val _ = Theory.setup
  18.267 -  (Document_Antiquotation.setup \<^binding>\<open>doc\<close> (Scan.lift (Parse.position Parse.embedded))
  18.268 -    (fn {context = ctxt, ...} => fn (name, pos) =>
  18.269 -      (Context_Position.report ctxt pos (Markup.doc name);
  18.270 -        Thy_Output.output ctxt [Thy_Output.pretty_text ctxt name])));
  18.271 +  (Thy_Output.antiquotation_raw \<^binding>\<open>url\<close> (Scan.lift (Parse.position Parse.embedded))
  18.272 +    (fn ctxt => fn (url, pos) =>
  18.273 +      let val _ = Context_Position.reports ctxt [(pos, Markup.language_path), (pos, Markup.url url)]
  18.274 +      in Latex.enclose_block "\\url{" "}" [Latex.string url] end));
  18.275  
  18.276  
  18.277  (* formal entities *)
  18.278  
  18.279 -fun entity_antiquotation name check output =
  18.280 -  Document_Antiquotation.setup name (Scan.lift (Parse.position Args.name))
  18.281 -    (fn {context = ctxt, ...} => fn (name, pos) => (check ctxt (name, pos); output name));
  18.282 +local
  18.283 +
  18.284 +fun entity_antiquotation name check bg en =
  18.285 +  Thy_Output.antiquotation_raw name (Scan.lift (Parse.position Args.name))
  18.286 +    (fn ctxt => fn (name, pos) =>
  18.287 +      let val _ = check ctxt (name, pos)
  18.288 +      in Latex.enclose_block bg en [Latex.string (Output.output name)] end);
  18.289 +
  18.290 +in
  18.291  
  18.292  val _ =
  18.293    Theory.setup
  18.294 -   (entity_antiquotation \<^binding>\<open>command\<close> Outer_Syntax.check_command
  18.295 -     (enclose "\\isacommand{" "}" o Output.output) #>
  18.296 -    entity_antiquotation \<^binding>\<open>method\<close> Method.check_name
  18.297 -     (enclose "\\isa{" "}" o Output.output) #>
  18.298 -    entity_antiquotation \<^binding>\<open>attribute\<close> Attrib.check_name
  18.299 -     (enclose "\\isa{" "}" o Output.output));
  18.300 +   (entity_antiquotation \<^binding>\<open>command\<close> Outer_Syntax.check_command "\\isacommand{" "}" #>
  18.301 +    entity_antiquotation \<^binding>\<open>method\<close> Method.check_name "\\isa{" "}" #>
  18.302 +    entity_antiquotation \<^binding>\<open>attribute\<close> Attrib.check_name "\\isa{" "}");
  18.303  
  18.304  end;
  18.305 +
  18.306 +end;
    19.1 --- a/src/Pure/Thy/latex.ML	Fri Jan 19 15:50:17 2018 +0100
    19.2 +++ b/src/Pure/Thy/latex.ML	Fri Jan 19 20:11:14 2018 +0100
    19.3 @@ -11,12 +11,15 @@
    19.4    val text: string * Position.T -> text
    19.5    val block: text list -> text
    19.6    val enclose_body: string -> string -> text list -> text list
    19.7 +  val enclose_block: string -> string -> text list -> text
    19.8    val output_text: text list -> string
    19.9    val output_positions: Position.T -> text list -> string
   19.10    val output_name: string -> string
   19.11    val output_ascii: string -> string
   19.12    val output_symbols: Symbol.symbol list -> string
   19.13    val output_syms: string -> string
   19.14 +  val symbols: Symbol_Pos.T list -> text
   19.15 +  val symbols_output: Symbol_Pos.T list -> text
   19.16    val begin_delim: string -> string
   19.17    val end_delim: string -> string
   19.18    val begin_tag: string -> string
   19.19 @@ -76,6 +79,8 @@
   19.20    (if bg = "" then [] else [string bg]) @ body @
   19.21    (if en = "" then [] else [string en]);
   19.22  
   19.23 +fun enclose_block bg en = block o enclose_body bg en;
   19.24 +
   19.25  
   19.26  (* output name for LaTeX macros *)
   19.27  
   19.28 @@ -198,6 +203,10 @@
   19.29  
   19.30  end;
   19.31  
   19.32 +fun symbols syms = text (Symbol_Pos.content syms, #1 (Symbol_Pos.range syms));
   19.33 +fun symbols_output syms =
   19.34 +  text (output_symbols (map Symbol_Pos.symbol syms), #1 (Symbol_Pos.range syms));
   19.35 +
   19.36  
   19.37  (* tags *)
   19.38  
    20.1 --- a/src/Pure/Thy/markdown.ML	Fri Jan 19 15:50:17 2018 +0100
    20.2 +++ b/src/Pure/Thy/markdown.ML	Fri Jan 19 20:11:14 2018 +0100
    20.3 @@ -132,8 +132,8 @@
    20.4  fun block_source (Par lines) = maps line_source lines
    20.5    | block_source (List {body, ...}) = maps line_source (maps block_lines body);
    20.6  
    20.7 -fun block_range (Par lines) = Antiquote.range (maps line_content lines)
    20.8 -  | block_range (List {body, ...}) = Antiquote.range (maps line_source (maps block_lines body));
    20.9 +fun block_range (Par lines) = Antiquote.text_range (maps line_content lines)
   20.10 +  | block_range (List {body, ...}) = Antiquote.text_range (maps line_source (maps block_lines body));
   20.11  
   20.12  fun block_indent (List {indent, ...}) = indent
   20.13    | block_indent (Par (Line {indent, ...} :: _)) = indent
   20.14 @@ -204,7 +204,7 @@
   20.15  local
   20.16  
   20.17  val block_pos = #1 o block_range;
   20.18 -val item_pos = #1 o Antiquote.range o maps block_source;
   20.19 +val item_pos = #1 o Antiquote.text_range o maps block_source;
   20.20  
   20.21  fun line_reports depth (Line {bullet_pos, content, ...}) =
   20.22    cons (bullet_pos, Markup.markdown_bullet depth) #> append (text_reports content);
    21.1 --- a/src/Pure/Thy/sessions.scala	Fri Jan 19 15:50:17 2018 +0100
    21.2 +++ b/src/Pure/Thy/sessions.scala	Fri Jan 19 20:11:14 2018 +0100
    21.3 @@ -129,6 +129,7 @@
    21.4  
    21.5    sealed case class Base(
    21.6      pos: Position.T = Position.none,
    21.7 +    doc_names: List[String] = Nil,
    21.8      global_theories: Map[String, String] = Map.empty,
    21.9      loaded_theories: Graph[String, Outer_Syntax] = Graph.string,
   21.10      known: Known = Known.empty,
   21.11 @@ -221,6 +222,8 @@
   21.12        }
   21.13      }
   21.14  
   21.15 +    val doc_names = Doc.doc_names()
   21.16 +
   21.17      val session_bases =
   21.18        (Map.empty[String, Base] /: sessions_structure.imports_topological_order)({
   21.19          case (session_bases, session_name) =>
   21.20 @@ -328,6 +331,7 @@
   21.21              val base =
   21.22                Base(
   21.23                  pos = info.pos,
   21.24 +                doc_names = doc_names,
   21.25                  global_theories = global_theories,
   21.26                  loaded_theories = dependencies.loaded_theories,
   21.27                  known = known,
    22.1 --- a/src/Pure/Thy/thy_output.ML	Fri Jan 19 15:50:17 2018 +0100
    22.2 +++ b/src/Pure/Thy/thy_output.ML	Fri Jan 19 20:11:14 2018 +0100
    22.3 @@ -10,17 +10,27 @@
    22.4    val check_comments: Proof.context -> Symbol_Pos.T list -> unit
    22.5    val check_token_comments: Proof.context -> Token.T -> unit
    22.6    val output_token: Proof.context -> Token.T -> Latex.text list
    22.7 +  val output_source: Proof.context -> string -> Latex.text list
    22.8    val present_thy: theory -> (Toplevel.transition * Toplevel.state) list ->
    22.9      Token.T list -> Latex.text list
   22.10 -  val pretty_text: Proof.context -> string -> Pretty.T
   22.11    val pretty_term: Proof.context -> term -> Pretty.T
   22.12    val pretty_thm: Proof.context -> thm -> Pretty.T
   22.13 -  val str_of_source: Token.src -> string
   22.14 -  val maybe_pretty_source: (Proof.context -> 'a -> Pretty.T) -> Proof.context ->
   22.15 -    Token.src -> 'a list -> Pretty.T list
   22.16 -  val string_of_margin: Proof.context -> Pretty.T -> string
   22.17 -  val output: Proof.context -> Pretty.T list -> string
   22.18 -  val verbatim_text: Proof.context -> string -> string
   22.19 +  val lines: Latex.text list -> Latex.text list
   22.20 +  val isabelle: Proof.context -> Latex.text list -> Latex.text
   22.21 +  val isabelle_typewriter: Proof.context -> Latex.text list -> Latex.text
   22.22 +  val typewriter: Proof.context -> string -> Latex.text
   22.23 +  val verbatim: Proof.context -> string -> Latex.text
   22.24 +  val source: Proof.context -> Token.src -> Latex.text
   22.25 +  val pretty: Proof.context -> Pretty.T list -> Latex.text
   22.26 +  val pretty_source: Proof.context -> Token.src -> Pretty.T list -> Latex.text
   22.27 +  val antiquotation_pretty:
   22.28 +    binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T list) -> theory -> theory
   22.29 +  val antiquotation_pretty_source:
   22.30 +    binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T list) -> theory -> theory
   22.31 +  val antiquotation_raw:
   22.32 +    binding -> 'a context_parser -> (Proof.context -> 'a -> Latex.text) -> theory -> theory
   22.33 +  val antiquotation_verbatim:
   22.34 +    binding -> 'a context_parser -> (Proof.context -> 'a -> string) -> theory -> theory
   22.35  end;
   22.36  
   22.37  structure Thy_Output: THY_OUTPUT =
   22.38 @@ -35,9 +45,7 @@
   22.39  
   22.40      val _ = Context_Position.report ctxt pos (Markup.language_document (Input.is_delimited source));
   22.41  
   22.42 -    val output_antiquotes =
   22.43 -      map (fn ant =>
   22.44 -        Latex.text (Document_Antiquotation.evaluate ctxt ant, #1 (Antiquote.range [ant])));
   22.45 +    val output_antiquotes = maps (Document_Antiquotation.evaluate ctxt);
   22.46  
   22.47      fun output_line line =
   22.48        (if Markdown.line_is_item line then [Latex.string "\\item "] else []) @
   22.49 @@ -60,7 +68,7 @@
   22.50        in output_blocks blocks end
   22.51      else
   22.52        let
   22.53 -        val ants = Antiquote.parse pos (Symbol_Pos.trim_blanks syms);
   22.54 +        val ants = Antiquote.parse pos (trim (Symbol.is_blank o Symbol_Pos.symbol) syms);
   22.55          val reports = Antiquote.antiq_reports ants;
   22.56          val _ = Context_Position.reports ctxt (reports @ Markdown.text_reports ants);
   22.57        in output_antiquotes ants end
   22.58 @@ -71,11 +79,7 @@
   22.59  
   22.60  local
   22.61  
   22.62 -fun output_latex syms =
   22.63 -  [Latex.text (Symbol_Pos.content syms, #1 (Symbol_Pos.range syms))];
   22.64 -
   22.65 -fun output_symbols syms =
   22.66 -  [Latex.text (Latex.output_symbols (map Symbol_Pos.symbol syms), #1 (Symbol_Pos.range syms))];
   22.67 +val output_symbols = single o Latex.symbols_output;
   22.68  
   22.69  val output_symbols_antiq =
   22.70    (fn Antiquote.Text syms => output_symbols syms
   22.71 @@ -95,15 +99,17 @@
   22.72        let
   22.73          val body = Symbol_Pos.cartouche_content syms;
   22.74          val source = Input.source true (Symbol_Pos.implode body) (Symbol_Pos.range body);
   22.75 +        val ctxt' = ctxt
   22.76 +          |> Config.put Document_Antiquotation.thy_output_display false;
   22.77        in
   22.78 -        output_text ctxt {markdown = false} source
   22.79 +        output_text ctxt' {markdown = false} source
   22.80          |> Latex.enclose_body "%\n\\isamarkupcmt{" "%\n}"
   22.81        end
   22.82    | (SOME Comment.Cancel, _) =>
   22.83        output_symbols (Symbol_Pos.cartouche_content syms)
   22.84        |> Latex.enclose_body "%\n\\isamarkupcancel{" "}"
   22.85    | (SOME Comment.Latex, _) =>
   22.86 -      output_latex (Symbol_Pos.cartouche_content syms));
   22.87 +      [Latex.symbols (Symbol_Pos.cartouche_content syms)]);
   22.88  
   22.89  in
   22.90  
   22.91 @@ -130,6 +136,9 @@
   22.92      | _ => output false "" "")
   22.93    end handle ERROR msg => error (msg ^ Position.here (Token.pos_of tok));
   22.94  
   22.95 +fun output_source ctxt s =
   22.96 +  output_body ctxt false "" "" (Symbol_Pos.explode (s, Position.none));
   22.97 +
   22.98  fun check_comments ctxt =
   22.99    Comment.read_body #> (Option.app o List.app) (fn (comment, syms) =>
  22.100      let
  22.101 @@ -425,58 +434,66 @@
  22.102  
  22.103  (** standard output operations **)
  22.104  
  22.105 -(* basic pretty printing *)
  22.106 +(* pretty printing *)
  22.107  
  22.108 -fun perhaps_trim ctxt =
  22.109 -  not (Config.get ctxt Document_Antiquotation.thy_output_display) ? Symbol.trim_blanks;
  22.110 -
  22.111 -fun pretty_text ctxt =
  22.112 -  Pretty.chunks o map Pretty.str o map (perhaps_trim ctxt) o split_lines;
  22.113 -
  22.114 -fun pretty_term ctxt t = Syntax.pretty_term (Variable.auto_fixes t ctxt) t;
  22.115 +fun pretty_term ctxt t =
  22.116 +  Syntax.pretty_term (Variable.auto_fixes t ctxt) t;
  22.117  
  22.118  fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of;
  22.119  
  22.120  
  22.121  (* default output *)
  22.122  
  22.123 -val str_of_source = space_implode " " o map Token.unparse o Token.args_of_src;
  22.124 +val lines = separate (Latex.string "\\isasep\\isanewline%\n");
  22.125  
  22.126 -fun maybe_pretty_source pretty ctxt src xs =
  22.127 -  map (pretty ctxt) xs  (*always pretty in order to exhibit errors!*)
  22.128 -  |> (if Config.get ctxt Document_Antiquotation.thy_output_source
  22.129 -      then K [pretty_text ctxt (str_of_source src)] else I);
  22.130 +fun isabelle ctxt body =
  22.131 +  if Config.get ctxt Document_Antiquotation.thy_output_display
  22.132 +  then Latex.environment_block "isabelle" body
  22.133 +  else Latex.block (Latex.enclose_body "\\isa{" "}" body);
  22.134  
  22.135 -fun string_of_margin ctxt =
  22.136 -  Pretty.string_of_margin (Config.get ctxt Document_Antiquotation.thy_output_margin);
  22.137 +fun isabelle_typewriter ctxt body =
  22.138 +  if Config.get ctxt Document_Antiquotation.thy_output_display
  22.139 +  then Latex.environment_block "isabellett" body
  22.140 +  else Latex.block (Latex.enclose_body "\\isatt{" "}" body);
  22.141  
  22.142 -fun output ctxt prts =
  22.143 -  prts
  22.144 -  |> Config.get ctxt Document_Antiquotation.thy_output_quotes ? map Pretty.quote
  22.145 -  |> (if Config.get ctxt Document_Antiquotation.thy_output_display then
  22.146 -        map (Pretty.indent (Config.get ctxt Document_Antiquotation.thy_output_indent)
  22.147 -          #> string_of_margin ctxt #> Output.output)
  22.148 -        #> space_implode "\\isasep\\isanewline%\n"
  22.149 -        #> Latex.environment "isabelle"
  22.150 -      else
  22.151 -        map
  22.152 -          ((if Config.get ctxt Document_Antiquotation.thy_output_break
  22.153 -            then string_of_margin ctxt else Pretty.unformatted_string_of) #> Output.output)
  22.154 -        #> space_implode "\\isasep\\isanewline%\n"
  22.155 -        #> enclose "\\isa{" "}");
  22.156 +fun typewriter ctxt s =
  22.157 +  isabelle_typewriter ctxt [Latex.string (Latex.output_ascii s)];
  22.158  
  22.159 +fun verbatim ctxt =
  22.160 +  if Config.get ctxt Document_Antiquotation.thy_output_display
  22.161 +  then Document_Antiquotation.indent_lines ctxt #> typewriter ctxt
  22.162 +  else split_lines #> map (typewriter ctxt) #> lines #> Latex.block;
  22.163  
  22.164 -(* verbatim text *)
  22.165 +fun source ctxt =
  22.166 +  Token.args_of_src
  22.167 +  #> map (Token.unparse #> Document_Antiquotation.prepare_lines ctxt)
  22.168 +  #> space_implode " "
  22.169 +  #> output_source ctxt
  22.170 +  #> isabelle ctxt;
  22.171  
  22.172 -fun verbatim_text ctxt =
  22.173 -  if Config.get ctxt Document_Antiquotation.thy_output_display then
  22.174 -    split_lines #>
  22.175 -    map (prefix (Symbol.spaces (Config.get ctxt Document_Antiquotation.thy_output_indent))) #>
  22.176 -    cat_lines #>
  22.177 -    Latex.output_ascii #> Latex.environment "isabellett"
  22.178 -  else
  22.179 -    split_lines #>
  22.180 -    map (Latex.output_ascii #> enclose "\\isatt{" "}") #>
  22.181 -    space_implode "\\isasep\\isanewline%\n";
  22.182 +fun pretty ctxt =
  22.183 +  map (Document_Antiquotation.output ctxt #> Latex.string) #> lines #> isabelle ctxt;
  22.184 +
  22.185 +fun pretty_source ctxt src prts =
  22.186 +  if Config.get ctxt Document_Antiquotation.thy_output_source
  22.187 +  then source ctxt src else pretty ctxt prts;
  22.188 +
  22.189 +
  22.190 +(* antiquotation variants *)
  22.191 +
  22.192 +fun antiquotation_pretty name scan f =
  22.193 +  Document_Antiquotation.setup name scan
  22.194 +    (fn {context = ctxt, argument = x, ...} => pretty ctxt (f ctxt x));
  22.195 +
  22.196 +fun antiquotation_pretty_source name scan f =
  22.197 +  Document_Antiquotation.setup name scan
  22.198 +    (fn {context = ctxt, source = src, argument = x} => pretty_source ctxt src (f ctxt x));
  22.199 +
  22.200 +fun antiquotation_raw name scan f =
  22.201 +  Document_Antiquotation.setup name scan
  22.202 +    (fn {context = ctxt, argument = x, ...} => f ctxt x);
  22.203 +
  22.204 +fun antiquotation_verbatim name scan f =
  22.205 +  antiquotation_raw name scan (fn ctxt => verbatim ctxt o f ctxt);
  22.206  
  22.207  end;
    23.1 --- a/src/Pure/Tools/build.ML	Fri Jan 19 15:50:17 2018 +0100
    23.2 +++ b/src/Pure/Tools/build.ML	Fri Jan 19 20:11:14 2018 +0100
    23.3 @@ -150,6 +150,7 @@
    23.4    master_dir: Path.T,
    23.5    theories: (Options.T * (string * Position.T) list) list,
    23.6    sessions: string list,
    23.7 +  doc_names: string list,
    23.8    global_theories: (string * string) list,
    23.9    loaded_theories: string list,
   23.10    known_theories: (string * string) list,
   23.11 @@ -161,14 +162,14 @@
   23.12      val position = Position.of_properties o properties;
   23.13      val (symbol_codes, (command_timings, (do_output, (verbose, (browser_info,
   23.14        (document_files, (graph_file, (parent_name, (chapter, (name, (master_dir,
   23.15 -      (theories, (sessions, (global_theories, (loaded_theories,
   23.16 -      (known_theories, bibtex_entries)))))))))))))))) =
   23.17 +      (theories, (sessions, (doc_names, (global_theories, (loaded_theories,
   23.18 +      (known_theories, bibtex_entries))))))))))))))))) =
   23.19        pair (list (pair string int)) (pair (list properties) (pair bool (pair bool (pair string
   23.20          (pair (list (pair string string)) (pair string (pair string (pair string (pair string
   23.21            (pair string
   23.22              (pair (((list (pair Options.decode (list (pair string position))))))
   23.23 -              (pair (list string) (pair (list (pair string string)) (pair (list string)
   23.24 -                (pair (list (pair string string)) (list string))))))))))))))))
   23.25 +              (pair (list string) (pair (list string) (pair (list (pair string string)) (pair (list string)
   23.26 +                (pair (list (pair string string)) (list string)))))))))))))))))
   23.27        (YXML.parse_body yxml);
   23.28    in
   23.29      Args {symbol_codes = symbol_codes, command_timings = command_timings, do_output = do_output,
   23.30 @@ -176,19 +177,20 @@
   23.31        document_files = map (apply2 Path.explode) document_files,
   23.32        graph_file = Path.explode graph_file, parent_name = parent_name, chapter = chapter,
   23.33        name = name, master_dir = Path.explode master_dir, theories = theories, sessions = sessions,
   23.34 -      global_theories = global_theories, loaded_theories = loaded_theories,
   23.35 +      doc_names = doc_names, global_theories = global_theories, loaded_theories = loaded_theories,
   23.36        known_theories = known_theories, bibtex_entries = bibtex_entries}
   23.37    end;
   23.38  
   23.39  fun build_session (Args {symbol_codes, command_timings, do_output, verbose, browser_info,
   23.40      document_files, graph_file, parent_name, chapter, name, master_dir, theories, sessions,
   23.41 -    global_theories, loaded_theories, known_theories, bibtex_entries}) =
   23.42 +    doc_names, global_theories, loaded_theories, known_theories, bibtex_entries}) =
   23.43    let
   23.44      val symbols = HTML.make_symbols symbol_codes;
   23.45  
   23.46      val _ =
   23.47        Resources.init_session_base
   23.48          {sessions = sessions,
   23.49 +         doc_names = doc_names,
   23.50           global_theories = global_theories,
   23.51           loaded_theories = loaded_theories,
   23.52           known_theories = known_theories};
    24.1 --- a/src/Pure/Tools/build.scala	Fri Jan 19 15:50:17 2018 +0100
    24.2 +++ b/src/Pure/Tools/build.scala	Fri Jan 19 20:11:14 2018 +0100
    24.3 @@ -212,16 +212,14 @@
    24.4                  pair(Path.encode, pair(list(pair(Path.encode, Path.encode)), pair(string,
    24.5                  pair(string, pair(string, pair(string, pair(Path.encode,
    24.6                  pair(list(pair(Options.encode, list(pair(string, properties)))),
    24.7 -                pair(list(string), pair(list(pair(string, string)), pair(list(string),
    24.8 -                pair(list(pair(string, string)), list(string)))))))))))))))))(
    24.9 +                pair(list(string), pair(list(string), pair(list(pair(string, string)),
   24.10 +                pair(list(string), pair(list(pair(string, string)), list(string))))))))))))))))))(
   24.11                (Symbol.codes, (command_timings, (do_output, (verbose,
   24.12                  (store.browser_info, (info.document_files, (File.standard_path(graph_file),
   24.13                  (parent, (info.chapter, (name, (Path.current,
   24.14 -                (info.theories, (base.known.sessions.toList,
   24.15 -                (base.global_theories.toList,
   24.16 -                (base.loaded_theories.keys,
   24.17 -                (base.dest_known_theories,
   24.18 -                info.bibtex_entries.map(_.info))))))))))))))))))
   24.19 +                (info.theories, (base.known.sessions.toList, (base.doc_names,
   24.20 +                (base.global_theories.toList, (base.loaded_theories.keys, (base.dest_known_theories,
   24.21 +                info.bibtex_entries.map(_.info)))))))))))))))))))
   24.22              })
   24.23  
   24.24          val env =
    25.1 --- a/src/Pure/Tools/doc.scala	Fri Jan 19 15:50:17 2018 +0100
    25.2 +++ b/src/Pure/Tools/doc.scala	Fri Jan 19 20:11:14 2018 +0100
    25.3 @@ -77,6 +77,9 @@
    25.4      examples() ::: release_notes() ::: main_contents
    25.5    }
    25.6  
    25.7 +  def doc_names(): List[String] =
    25.8 +    for (Doc(name, _, _) <- contents()) yield name
    25.9 +
   25.10  
   25.11    /* view */
   25.12  
    26.1 --- a/src/Pure/Tools/jedit.ML	Fri Jan 19 15:50:17 2018 +0100
    26.2 +++ b/src/Pure/Tools/jedit.ML	Fri Jan 19 20:11:14 2018 +0100
    26.3 @@ -75,10 +75,14 @@
    26.4  
    26.5  val _ =
    26.6    Theory.setup
    26.7 -    (Document_Antiquotation.setup \<^binding>\<open>action\<close> (Scan.lift (Parse.position Parse.embedded))
    26.8 -      (fn {context = ctxt, ...} => fn (name, pos) =>
    26.9 -       (if Context_Position.is_reported ctxt pos then ignore (check_action (name, pos)) else ();
   26.10 -        Thy_Output.verbatim_text ctxt name)));
   26.11 +    (Thy_Output.antiquotation_verbatim \<^binding>\<open>action\<close> (Scan.lift (Parse.position Parse.embedded))
   26.12 +      (fn ctxt => fn (name, pos) =>
   26.13 +        let
   26.14 +          val _ =
   26.15 +            if Context_Position.is_reported ctxt pos
   26.16 +            then ignore (check_action (name, pos))
   26.17 +            else ();
   26.18 +        in name end));
   26.19  
   26.20  end;
   26.21  
    27.1 --- a/src/Pure/Tools/rail.ML	Fri Jan 19 15:50:17 2018 +0100
    27.2 +++ b/src/Pure/Tools/rail.ML	Fri Jan 19 20:11:14 2018 +0100
    27.3 @@ -17,7 +17,7 @@
    27.4      Terminal of bool * string |
    27.5      Antiquote of bool * Antiquote.antiq
    27.6    val read: Proof.context -> Input.source -> (string Antiquote.antiquote * rail) list
    27.7 -  val output_rules: Proof.context -> (string Antiquote.antiquote * rail) list -> string
    27.8 +  val output_rules: Proof.context -> (string Antiquote.antiquote * rail) list -> Latex.text
    27.9  end;
   27.10  
   27.11  structure Rail: RAIL =
   27.12 @@ -339,7 +339,8 @@
   27.13  
   27.14  fun output_rules ctxt rules =
   27.15    let
   27.16 -    val output_antiq = Document_Antiquotation.evaluate ctxt o Antiquote.Antiq;
   27.17 +    val output_antiq =
   27.18 +      Latex.output_text o Document_Antiquotation.evaluate ctxt o Antiquote.Antiq;
   27.19      fun output_text b s =
   27.20        Output.output s
   27.21        |> b ? enclose "\\isakeyword{" "}"
   27.22 @@ -378,11 +379,11 @@
   27.23          output "" rail' ^
   27.24          "\\rail@end\n"
   27.25        end;
   27.26 -  in Latex.environment "railoutput" (implode (map output_rule rules)) end;
   27.27 +  in Latex.string (Latex.environment "railoutput" (implode (map output_rule rules))) end;
   27.28  
   27.29  val _ = Theory.setup
   27.30 -  (Document_Antiquotation.setup \<^binding>\<open>rail\<close> (Scan.lift Args.text_input)
   27.31 -    (fn {context = ctxt, ...} => output_rules ctxt o read ctxt));
   27.32 +  (Thy_Output.antiquotation_raw \<^binding>\<open>rail\<close> (Scan.lift Args.text_input)
   27.33 +    (fn ctxt => output_rules ctxt o read ctxt));
   27.34  
   27.35  end;
   27.36  
    28.1 --- a/src/Tools/Code/code_target.ML	Fri Jan 19 15:50:17 2018 +0100
    28.2 +++ b/src/Tools/Code/code_target.ML	Fri Jan 19 20:11:14 2018 +0100
    28.3 @@ -510,14 +510,15 @@
    28.4  in
    28.5  
    28.6  val _ = Theory.setup
    28.7 -  (Document_Antiquotation.setup @{binding code_stmts}
    28.8 +  (Thy_Output.antiquotation_raw @{binding code_stmts}
    28.9      (parse_const_terms --
   28.10        Scan.repeat (parse_consts || parse_types || parse_classes || parse_instances)
   28.11        -- Scan.lift (Args.parens (Args.name -- Scan.option Parse.int)))
   28.12 -    (fn {context = ctxt, ...} => fn ((mk_cs, mk_stmtss), (target_name, some_width)) =>
   28.13 -        present_code ctxt (mk_cs ctxt)
   28.14 +    (fn ctxt => fn ((mk_cs, mk_stmtss), (target_name, some_width)) =>
   28.15 +      Latex.string
   28.16 +        (present_code ctxt (mk_cs ctxt)
   28.17            (maps (fn f => f ctxt) mk_stmtss)
   28.18 -          target_name some_width "Example" []));
   28.19 +          target_name some_width "Example" [])));
   28.20  
   28.21  end;
   28.22