clarified modules;
authorwenzelm
Tue Jan 09 15:40:12 2018 +0100 (22 months ago)
changeset 67386998e01d6f8fd
parent 67385 deb9b0283259
child 67387 ff07dd9c7cb4
clarified modules;
src/Doc/Main/Main_Doc.thy
src/Doc/Prog_Prove/LaTeXsugar.thy
src/Doc/antiquote_setup.ML
src/Doc/more_antiquote.ML
src/HOL/Library/LaTeXsugar.thy
src/HOL/Tools/BNF/bnf_fp_util.ML
src/HOL/Tools/value_command.ML
src/Pure/PIDE/resources.ML
src/Pure/Pure.thy
src/Pure/ROOT.ML
src/Pure/Thy/bibtex.ML
src/Pure/Thy/document_antiquotation.ML
src/Pure/Thy/document_antiquotations.ML
src/Pure/Thy/thy_output.ML
src/Pure/Tools/jedit.ML
src/Pure/Tools/rail.ML
src/Tools/Code/code_target.ML
     1.1 --- a/src/Doc/Main/Main_Doc.thy	Tue Jan 09 15:18:41 2018 +0100
     1.2 +++ b/src/Doc/Main/Main_Doc.thy	Tue Jan 09 15:40:12 2018 +0100
     1.3 @@ -10,7 +10,7 @@
     1.4         else error "term_type_only: type mismatch";
     1.5         Syntax.pretty_typ ctxt T)
     1.6    in
     1.7 -    Thy_Output.antiquotation @{binding term_type_only}
     1.8 +    Document_Antiquotation.setup @{binding term_type_only}
     1.9        (Args.term -- Args.typ_abbrev)
    1.10        (fn {source, context = ctxt, ...} => fn arg =>
    1.11          Thy_Output.output ctxt
    1.12 @@ -18,7 +18,7 @@
    1.13    end
    1.14  \<close>
    1.15  setup \<open>
    1.16 -  Thy_Output.antiquotation @{binding expanded_typ} (Args.typ >> single)
    1.17 +  Document_Antiquotation.setup @{binding expanded_typ} (Args.typ >> single)
    1.18      (fn {source, context, ...} => Thy_Output.output context o
    1.19        Thy_Output.maybe_pretty_source Syntax.pretty_typ context source)
    1.20  \<close>
     2.1 --- a/src/Doc/Prog_Prove/LaTeXsugar.thy	Tue Jan 09 15:18:41 2018 +0100
     2.2 +++ b/src/Doc/Prog_Prove/LaTeXsugar.thy	Tue Jan 09 15:40:12 2018 +0100
     2.3 @@ -51,7 +51,7 @@
     2.4              Pretty.brk 1, Syntax.pretty_typ ctxt (fastype_of tc)]
     2.5        end
     2.6    in
     2.7 -    Thy_Output.antiquotation @{binding "const_typ"}
     2.8 +    Document_Antiquotation.setup @{binding "const_typ"}
     2.9       (Scan.lift Args.embedded_inner_syntax)
    2.10         (fn {source = src, context = ctxt, ...} => fn arg =>
    2.11            Thy_Output.output ctxt
     3.1 --- a/src/Doc/antiquote_setup.ML	Tue Jan 09 15:18:41 2018 +0100
     3.2 +++ b/src/Doc/antiquote_setup.ML	Tue Jan 09 15:40:12 2018 +0100
     3.3 @@ -73,7 +73,7 @@
     3.4  fun prep_ml source =
     3.5    (Input.source_content source, ML_Lex.read_source false source);
     3.6  
     3.7 -fun index_ml name kind ml = Thy_Output.antiquotation name
     3.8 +fun index_ml name kind ml = Document_Antiquotation.setup name
     3.9    (Scan.lift (Args.text_input -- Scan.option (Args.colon |-- Args.text_input)))
    3.10    (fn {context = ctxt, ...} => fn (source1, opt_source2) =>
    3.11      let
    3.12 @@ -119,17 +119,18 @@
    3.13  (* named theorems *)
    3.14  
    3.15  val _ =
    3.16 -  Theory.setup (Thy_Output.antiquotation @{binding named_thms}
    3.17 +  Theory.setup (Document_Antiquotation.setup @{binding named_thms}
    3.18      (Scan.repeat (Attrib.thm -- Scan.lift (Args.parens Args.name)))
    3.19      (fn {context = ctxt, ...} =>
    3.20        map (apfst (Thy_Output.pretty_thm ctxt))
    3.21 -      #> (if Config.get ctxt Thy_Output.quotes then map (apfst Pretty.quote) else I)
    3.22 -      #> (if Config.get ctxt Thy_Output.display
    3.23 +      #> (if Config.get ctxt Document_Antiquotation.thy_output_quotes
    3.24 +          then map (apfst Pretty.quote) else I)
    3.25 +      #> (if Config.get ctxt Document_Antiquotation.thy_output_display
    3.26            then
    3.27              map (fn (p, name) =>
    3.28                Output.output
    3.29                  (Thy_Output.string_of_margin ctxt
    3.30 -                  (Pretty.indent (Config.get ctxt Thy_Output.indent) p)) ^
    3.31 +                  (Pretty.indent (Config.get ctxt Document_Antiquotation.thy_output_indent) p)) ^
    3.32                "\\rulename{" ^
    3.33                Output.output (Pretty.unformatted_string_of (Thy_Output.pretty_text ctxt name)) ^ "}")
    3.34              #> space_implode "\\par\\smallskip%\n"
    3.35 @@ -160,7 +161,7 @@
    3.36  val arg = enclose "{" "}" o clean_string;
    3.37  
    3.38  fun entity check markup binding index =
    3.39 -  Thy_Output.antiquotation
    3.40 +  Document_Antiquotation.setup
    3.41      (binding |> Binding.map_name (fn name => name ^
    3.42        (case index of NONE => "" | SOME true => "_def" | SOME false => "_ref")))
    3.43      (Scan.lift (Scan.optional (Args.parens Args.name) "" -- Parse.position Args.name))
    3.44 @@ -204,8 +205,8 @@
    3.45      entity_antiqs no_check "" @{binding fact} #>
    3.46      entity_antiqs no_check "" @{binding variable} #>
    3.47      entity_antiqs no_check "" @{binding case} #>
    3.48 -    entity_antiqs Thy_Output.check_command "" @{binding antiquotation} #>
    3.49 -    entity_antiqs Thy_Output.check_option "" @{binding antiquotation_option} #>
    3.50 +    entity_antiqs Document_Antiquotation.check "" @{binding antiquotation} #>
    3.51 +    entity_antiqs Document_Antiquotation.check_option "" @{binding antiquotation_option} #>
    3.52      entity_antiqs no_check "isasystem" @{binding setting} #>
    3.53      entity_antiqs check_system_option "isasystem" @{binding system_option} #>
    3.54      entity_antiqs no_check "" @{binding inference} #>
     4.1 --- a/src/Doc/more_antiquote.ML	Tue Jan 09 15:18:41 2018 +0100
     4.2 +++ b/src/Doc/more_antiquote.ML	Tue Jan 09 15:40:12 2018 +0100
     4.3 @@ -20,7 +20,7 @@
     4.4  in
     4.5  
     4.6  val _ =
     4.7 -  Theory.setup (Thy_Output.antiquotation @{binding class_spec} (Scan.lift Args.name)
     4.8 +  Theory.setup (Document_Antiquotation.setup @{binding class_spec} (Scan.lift Args.name)
     4.9      (fn {context, ...} => class_spec context));
    4.10  
    4.11  end;
    4.12 @@ -53,7 +53,7 @@
    4.13  in
    4.14  
    4.15  val _ =
    4.16 -  Theory.setup (Thy_Output.antiquotation @{binding code_thms} Args.term
    4.17 +  Theory.setup (Document_Antiquotation.setup @{binding code_thms} Args.term
    4.18      (fn {context, ...} => pretty_code_thm context));
    4.19  
    4.20  end;
     5.1 --- a/src/HOL/Library/LaTeXsugar.thy	Tue Jan 09 15:18:41 2018 +0100
     5.2 +++ b/src/HOL/Library/LaTeXsugar.thy	Tue Jan 09 15:40:12 2018 +0100
     5.3 @@ -104,7 +104,7 @@
     5.4              Pretty.brk 1, Syntax.pretty_typ ctxt (fastype_of tc)]
     5.5        end
     5.6    in
     5.7 -    Thy_Output.antiquotation @{binding "const_typ"}
     5.8 +    Document_Antiquotation.setup @{binding "const_typ"}
     5.9       (Scan.lift Args.embedded_inner_syntax)
    5.10         (fn {source = src, context = ctxt, ...} => fn arg =>
    5.11            Thy_Output.output ctxt
     6.1 --- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Tue Jan 09 15:18:41 2018 +0100
     6.2 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Tue Jan 09 15:40:12 2018 +0100
     6.3 @@ -983,7 +983,7 @@
     6.4    end;
     6.5  
     6.6  fun fp_antiquote_setup binding =
     6.7 -  Thy_Output.antiquotation binding (Args.type_name {proper = true, strict = true})
     6.8 +  Document_Antiquotation.setup binding (Args.type_name {proper = true, strict = true})
     6.9      (fn {source = src, context = ctxt, ...} => fn fcT_name =>
    6.10         (case Ctr_Sugar.ctr_sugar_of ctxt fcT_name of
    6.11           NONE => error ("Not a known freely generated type name: " ^ quote fcT_name)
     7.1 --- a/src/HOL/Tools/value_command.ML	Tue Jan 09 15:18:41 2018 +0100
     7.2 +++ b/src/HOL/Tools/value_command.ML	Tue Jan 09 15:40:12 2018 +0100
     7.3 @@ -73,7 +73,7 @@
     7.4        >> (fn ((name, modes), t) => Toplevel.keep (value_cmd name modes t)));
     7.5  
     7.6  val _ = Theory.setup
     7.7 -  (Thy_Output.antiquotation \<^binding>\<open>value\<close>
     7.8 +  (Document_Antiquotation.setup \<^binding>\<open>value\<close>
     7.9      (Scan.lift opt_evaluator -- Term_Style.parse -- Args.term)
    7.10      (fn {source, context, ...} => fn ((name, style), t) => Thy_Output.output context
    7.11        (Thy_Output.maybe_pretty_source Thy_Output.pretty_term context source
     8.1 --- a/src/Pure/PIDE/resources.ML	Tue Jan 09 15:18:41 2018 +0100
     8.2 +++ b/src/Pure/PIDE/resources.ML	Tue Jan 09 15:40:12 2018 +0100
     8.3 @@ -257,13 +257,13 @@
     8.4  in
     8.5  
     8.6  val _ = Theory.setup
     8.7 - (Thy_Output.antiquotation \<^binding>\<open>session\<close> (Scan.lift (Parse.position Parse.embedded))
     8.8 + (Document_Antiquotation.setup \<^binding>\<open>session\<close> (Scan.lift (Parse.position Parse.embedded))
     8.9      (fn {context = ctxt, ...} => Thy_Output.verbatim_text ctxt o check_session ctxt) #>
    8.10 -  Thy_Output.antiquotation \<^binding>\<open>path\<close> (Scan.lift (Parse.position Parse.path))
    8.11 +  Document_Antiquotation.setup \<^binding>\<open>path\<close> (Scan.lift (Parse.position Parse.path))
    8.12      (document_antiq check_path o #context) #>
    8.13 -  Thy_Output.antiquotation \<^binding>\<open>file\<close> (Scan.lift (Parse.position Parse.path))
    8.14 +  Document_Antiquotation.setup \<^binding>\<open>file\<close> (Scan.lift (Parse.position Parse.path))
    8.15      (document_antiq check_file o #context) #>
    8.16 -  Thy_Output.antiquotation \<^binding>\<open>dir\<close> (Scan.lift (Parse.position Parse.path))
    8.17 +  Document_Antiquotation.setup \<^binding>\<open>dir\<close> (Scan.lift (Parse.position Parse.path))
    8.18      (document_antiq check_dir o #context) #>
    8.19    ML_Antiquotation.value \<^binding>\<open>path\<close>
    8.20      (Args.context -- Scan.lift (Parse.position Parse.path) >> uncurry (ML_antiq check_path)) #>
     9.1 --- a/src/Pure/Pure.thy	Tue Jan 09 15:18:41 2018 +0100
     9.2 +++ b/src/Pure/Pure.thy	Tue Jan 09 15:40:12 2018 +0100
     9.3 @@ -1145,7 +1145,7 @@
     9.4    Outer_Syntax.command \<^command_keyword>\<open>print_antiquotations\<close>
     9.5      "print document antiquotations"
     9.6      (Parse.opt_bang >> (fn b =>
     9.7 -      Toplevel.keep (Thy_Output.print_antiquotations b o Toplevel.context_of)));
     9.8 +      Toplevel.keep (Document_Antiquotation.print_antiquotations b o Toplevel.context_of)));
     9.9  
    9.10  val _ =
    9.11    Outer_Syntax.command \<^command_keyword>\<open>print_ML_antiquotations\<close>
    10.1 --- a/src/Pure/ROOT.ML	Tue Jan 09 15:18:41 2018 +0100
    10.2 +++ b/src/Pure/ROOT.ML	Tue Jan 09 15:40:12 2018 +0100
    10.3 @@ -281,6 +281,7 @@
    10.4  ML_file "Thy/term_style.ML";
    10.5  ML_file "Isar/outer_syntax.ML";
    10.6  ML_file "ML/ml_antiquotations.ML";
    10.7 +ML_file "Thy/document_antiquotation.ML";
    10.8  ML_file "Thy/thy_output.ML";
    10.9  ML_file "Thy/document_antiquotations.ML";
   10.10  ML_file "General/graph_display.ML";
    11.1 --- a/src/Pure/Thy/bibtex.ML	Tue Jan 09 15:18:41 2018 +0100
    11.2 +++ b/src/Pure/Thy/bibtex.ML	Tue Jan 09 15:40:12 2018 +0100
    11.3 @@ -40,8 +40,8 @@
    11.4  
    11.5  val _ =
    11.6    Theory.setup
    11.7 -   (Thy_Output.add_option \<^binding>\<open>cite_macro\<close> (Config.put cite_macro) #>
    11.8 -    Thy_Output.antiquotation \<^binding>\<open>cite\<close>
    11.9 +   (Document_Antiquotation.setup_option \<^binding>\<open>cite_macro\<close> (Config.put cite_macro) #>
   11.10 +    Document_Antiquotation.setup \<^binding>\<open>cite\<close>
   11.11        (Scan.lift
   11.12          (Scan.option (Parse.verbatim || Parse.cartouche) --
   11.13           Parse.and_list1 (Parse.position Args.name)))
    12.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.2 +++ b/src/Pure/Thy/document_antiquotation.ML	Tue Jan 09 15:40:12 2018 +0100
    12.3 @@ -0,0 +1,184 @@
    12.4 +(*  Title:      Pure/Thy/document_antiquotation.ML
    12.5 +    Author:     Makarius
    12.6 +
    12.7 +Document antiquotations.
    12.8 +*)
    12.9 +
   12.10 +signature DOCUMENT_ANTIQUOTATION =
   12.11 +sig
   12.12 +  val thy_output_display: bool Config.T
   12.13 +  val thy_output_quotes: bool Config.T
   12.14 +  val thy_output_margin: int Config.T
   12.15 +  val thy_output_indent: int Config.T
   12.16 +  val thy_output_source: bool Config.T
   12.17 +  val thy_output_break: bool Config.T
   12.18 +  val thy_output_modes: string Config.T
   12.19 +  val add_wrapper: ((unit -> string) -> unit -> string) -> Proof.context -> Proof.context
   12.20 +  val print_antiquotations: bool -> Proof.context -> unit
   12.21 +  val check: Proof.context -> xstring * Position.T -> string
   12.22 +  val check_option: Proof.context -> xstring * Position.T -> string
   12.23 +  val setup: binding -> 'a context_parser ->
   12.24 +    ({source: Token.src, context: Proof.context} -> 'a -> string) -> theory -> theory
   12.25 +  val setup_option: binding -> (string -> Proof.context -> Proof.context) -> theory -> theory
   12.26 +  val boolean: string -> bool
   12.27 +  val integer: string -> int
   12.28 +  val evaluate: Proof.context -> Antiquote.text_antiquote -> string
   12.29 +end;
   12.30 +
   12.31 +structure Document_Antiquotation: DOCUMENT_ANTIQUOTATION =
   12.32 +struct
   12.33 +
   12.34 +(* options *)
   12.35 +
   12.36 +val thy_output_display = Attrib.setup_option_bool ("thy_output_display", \<^here>);
   12.37 +val thy_output_break = Attrib.setup_option_bool ("thy_output_break", \<^here>);
   12.38 +val thy_output_quotes = Attrib.setup_option_bool ("thy_output_quotes", \<^here>);
   12.39 +val thy_output_margin = Attrib.setup_option_int ("thy_output_margin", \<^here>);
   12.40 +val thy_output_indent = Attrib.setup_option_int ("thy_output_indent", \<^here>);
   12.41 +val thy_output_source = Attrib.setup_option_bool ("thy_output_source", \<^here>);
   12.42 +val thy_output_modes = Attrib.setup_option_string ("thy_output_modes", \<^here>);
   12.43 +
   12.44 +
   12.45 +structure Wrappers = Proof_Data
   12.46 +(
   12.47 +  type T = ((unit -> string) -> unit -> string) list;
   12.48 +  fun init _ = [];
   12.49 +);
   12.50 +
   12.51 +fun add_wrapper wrapper = Wrappers.map (cons wrapper);
   12.52 +
   12.53 +val wrap = Wrappers.get #> fold (fn wrapper => fn f => wrapper f);
   12.54 +
   12.55 +
   12.56 +(* theory data *)
   12.57 +
   12.58 +structure Data = Theory_Data
   12.59 +(
   12.60 +  type T =
   12.61 +    (Token.src -> Proof.context -> string) Name_Space.table *
   12.62 +      (string -> Proof.context -> Proof.context) Name_Space.table;
   12.63 +  val empty : T =
   12.64 +    (Name_Space.empty_table Markup.document_antiquotationN,
   12.65 +      Name_Space.empty_table Markup.document_antiquotation_optionN);
   12.66 +  val extend = I;
   12.67 +  fun merge ((commands1, options1), (commands2, options2)) : T =
   12.68 +    (Name_Space.merge_tables (commands1, commands2),
   12.69 +      Name_Space.merge_tables (options1, options2));
   12.70 +);
   12.71 +
   12.72 +val get_antiquotations = Data.get o Proof_Context.theory_of;
   12.73 +
   12.74 +fun print_antiquotations verbose ctxt =
   12.75 +  let
   12.76 +    val (commands, options) = get_antiquotations ctxt;
   12.77 +    val command_names = map #1 (Name_Space.markup_table verbose ctxt commands);
   12.78 +    val option_names = map #1 (Name_Space.markup_table verbose ctxt options);
   12.79 +  in
   12.80 +    [Pretty.big_list "document antiquotations:" (map Pretty.mark_str command_names),
   12.81 +     Pretty.big_list "document antiquotation options:" (map Pretty.mark_str option_names)]
   12.82 +  end |> Pretty.writeln_chunks;
   12.83 +
   12.84 +fun check ctxt = #1 o Name_Space.check (Context.Proof ctxt) (#1 (get_antiquotations ctxt));
   12.85 +fun check_option ctxt = #1 o Name_Space.check (Context.Proof ctxt) (#2 (get_antiquotations ctxt));
   12.86 +
   12.87 +fun setup name scan body thy =
   12.88 +  let
   12.89 +    fun cmd src ctxt =
   12.90 +      let val (x, ctxt') = Token.syntax scan src ctxt
   12.91 +      in body {source = src, context = ctxt'} x end;
   12.92 +  in thy |> Data.map (apfst (Name_Space.define (Context.Theory thy) true (name, cmd) #> #2)) end;
   12.93 +
   12.94 +fun setup_option name opt thy = thy
   12.95 +  |> Data.map (apsnd (Name_Space.define (Context.Theory thy) true (name, opt) #> #2));
   12.96 +
   12.97 +
   12.98 +(* syntax *)
   12.99 +
  12.100 +local
  12.101 +
  12.102 +val property =
  12.103 +  Parse.position Parse.name -- Scan.optional (Parse.$$$ "=" |-- Parse.!!! Parse.name) "";
  12.104 +
  12.105 +val properties =
  12.106 +  Scan.optional (Parse.$$$ "[" |-- Parse.!!! (Parse.enum "," property --| Parse.$$$ "]")) [];
  12.107 +
  12.108 +in
  12.109 +
  12.110 +val antiq =
  12.111 +  Parse.!!!
  12.112 +    (Parse.token Parse.liberal_name -- properties -- Parse.args --| Scan.ahead Parse.eof)
  12.113 +  >> (fn ((name, props), args) => (props, name :: args));
  12.114 +
  12.115 +end;
  12.116 +
  12.117 +
  12.118 +(* evaluate *)
  12.119 +
  12.120 +local
  12.121 +
  12.122 +fun command src ctxt =
  12.123 +  let val (src', f) = Token.check_src ctxt (#1 o get_antiquotations) src
  12.124 +  in f src' ctxt end;
  12.125 +
  12.126 +fun option ((xname, pos), s) ctxt =
  12.127 +  let
  12.128 +    val (_, opt) =
  12.129 +      Name_Space.check (Context.Proof ctxt) (#2 (get_antiquotations ctxt)) (xname, pos);
  12.130 +  in opt s ctxt end;
  12.131 +
  12.132 +fun eval ctxt (opts, src) =
  12.133 +  let
  12.134 +    val preview_ctxt = fold option opts ctxt;
  12.135 +    val print_ctxt = Context_Position.set_visible false preview_ctxt;
  12.136 +
  12.137 +    fun cmd ctxt = wrap ctxt (fn () => command src ctxt) ();
  12.138 +    val _ = cmd preview_ctxt;
  12.139 +    val print_modes = space_explode "," (Config.get print_ctxt thy_output_modes) @ [Latex.latexN];
  12.140 +  in Print_Mode.with_modes print_modes (fn () => cmd print_ctxt) () end;
  12.141 +
  12.142 +in
  12.143 +
  12.144 +fun evaluate _ (Antiquote.Text ss) = Symbol_Pos.content ss
  12.145 +  | evaluate ctxt (Antiquote.Control {name, body, ...}) =
  12.146 +      eval ctxt ([], Token.make_src name (if null body then [] else [Token.read_cartouche body]))
  12.147 +  | evaluate ctxt (Antiquote.Antiq {range = (pos, _), body, ...}) =
  12.148 +      let val keywords = Thy_Header.get_keywords' ctxt;
  12.149 +      in eval ctxt (Token.read_antiq keywords antiq (body, pos)) end;
  12.150 +
  12.151 +end;
  12.152 +
  12.153 +
  12.154 +(* option syntax *)
  12.155 +
  12.156 +fun boolean "" = true
  12.157 +  | boolean "true" = true
  12.158 +  | boolean "false" = false
  12.159 +  | boolean s = error ("Bad boolean value: " ^ quote s);
  12.160 +
  12.161 +fun integer s =
  12.162 +  let
  12.163 +    fun int ss =
  12.164 +      (case Library.read_int ss of (i, []) => i
  12.165 +      | _ => error ("Bad integer value: " ^ quote s));
  12.166 +  in (case Symbol.explode s of "-" :: ss => ~ (int ss) | ss => int ss) end;
  12.167 +
  12.168 +val _ = Theory.setup
  12.169 + (setup_option \<^binding>\<open>show_types\<close> (Config.put show_types o boolean) #>
  12.170 +  setup_option \<^binding>\<open>show_sorts\<close> (Config.put show_sorts o boolean) #>
  12.171 +  setup_option \<^binding>\<open>show_structs\<close> (Config.put show_structs o boolean) #>
  12.172 +  setup_option \<^binding>\<open>show_question_marks\<close> (Config.put show_question_marks o boolean) #>
  12.173 +  setup_option \<^binding>\<open>show_abbrevs\<close> (Config.put show_abbrevs o boolean) #>
  12.174 +  setup_option \<^binding>\<open>names_long\<close> (Config.put Name_Space.names_long o boolean) #>
  12.175 +  setup_option \<^binding>\<open>names_short\<close> (Config.put Name_Space.names_short o boolean) #>
  12.176 +  setup_option \<^binding>\<open>names_unique\<close> (Config.put Name_Space.names_unique o boolean) #>
  12.177 +  setup_option \<^binding>\<open>eta_contract\<close> (Config.put Syntax_Trans.eta_contract o boolean) #>
  12.178 +  setup_option \<^binding>\<open>display\<close> (Config.put thy_output_display o boolean) #>
  12.179 +  setup_option \<^binding>\<open>break\<close> (Config.put thy_output_break o boolean) #>
  12.180 +  setup_option \<^binding>\<open>quotes\<close> (Config.put thy_output_quotes o boolean) #>
  12.181 +  setup_option \<^binding>\<open>mode\<close> (add_wrapper o Print_Mode.with_modes o single) #>
  12.182 +  setup_option \<^binding>\<open>margin\<close> (Config.put thy_output_margin o integer) #>
  12.183 +  setup_option \<^binding>\<open>indent\<close> (Config.put thy_output_indent o integer) #>
  12.184 +  setup_option \<^binding>\<open>source\<close> (Config.put thy_output_source o boolean) #>
  12.185 +  setup_option \<^binding>\<open>goals_limit\<close> (Config.put Goal_Display.goals_limit o integer));
  12.186 +
  12.187 +end;
    13.1 --- a/src/Pure/Thy/document_antiquotations.ML	Tue Jan 09 15:18:41 2018 +0100
    13.2 +++ b/src/Pure/Thy/document_antiquotations.ML	Tue Jan 09 15:40:12 2018 +0100
    13.3 @@ -7,12 +7,99 @@
    13.4  structure Document_Antiquotations: sig end =
    13.5  struct
    13.6  
    13.7 +(* basic entities *)
    13.8 +
    13.9 +local
   13.10 +
   13.11 +fun pretty_term_style ctxt (style, t: term) =
   13.12 +  Thy_Output.pretty_term ctxt (style t);
   13.13 +
   13.14 +fun pretty_thm_style ctxt (style, th) =
   13.15 +  Thy_Output.pretty_term ctxt (style (Thm.full_prop_of th));
   13.16 +
   13.17 +fun pretty_term_typ ctxt (style, t: term) =
   13.18 +  let val t' = style t
   13.19 +  in Thy_Output.pretty_term ctxt (Type.constraint (Term.fastype_of t') t') end;
   13.20 +
   13.21 +fun pretty_term_typeof ctxt (style, t) =
   13.22 +  Syntax.pretty_typ ctxt (Term.fastype_of (style t));
   13.23 +
   13.24 +fun pretty_const ctxt c =
   13.25 +  let
   13.26 +    val t = Const (c, Consts.type_scheme (Proof_Context.consts_of ctxt) c)
   13.27 +      handle TYPE (msg, _, _) => error msg;
   13.28 +    val ([t'], _) = Variable.import_terms true [t] ctxt;
   13.29 +  in Thy_Output.pretty_term ctxt t' end;
   13.30 +
   13.31 +fun pretty_abbrev ctxt s =
   13.32 +  let
   13.33 +    val t = Syntax.read_term (Proof_Context.set_mode Proof_Context.mode_abbrev ctxt) s;
   13.34 +    fun err () = error ("Abbreviated constant expected: " ^ Syntax.string_of_term ctxt t);
   13.35 +    val (head, args) = Term.strip_comb t;
   13.36 +    val (c, T) = Term.dest_Const head handle TERM _ => err ();
   13.37 +    val (U, u) = Consts.the_abbreviation (Proof_Context.consts_of ctxt) c
   13.38 +      handle TYPE _ => err ();
   13.39 +    val t' = Term.betapplys (Envir.expand_atom T (U, u), args);
   13.40 +    val eq = Logic.mk_equals (t, t');
   13.41 +    val ctxt' = Variable.auto_fixes eq ctxt;
   13.42 +  in Proof_Context.pretty_term_abbrev ctxt' eq end;
   13.43 +
   13.44 +fun pretty_locale ctxt (name, pos) =
   13.45 +  let
   13.46 +    val thy = Proof_Context.theory_of ctxt
   13.47 +  in (Pretty.str o Locale.extern thy o Locale.check thy) (name, pos) end;
   13.48 +
   13.49 +fun pretty_class ctxt =
   13.50 +  Pretty.str o Proof_Context.extern_class ctxt o Proof_Context.read_class ctxt;
   13.51 +
   13.52 +fun pretty_type ctxt s =
   13.53 +  let val Type (name, _) = Proof_Context.read_type_name {proper = true, strict = false} ctxt s
   13.54 +  in Pretty.str (Proof_Context.extern_type ctxt name) end;
   13.55 +
   13.56 +fun pretty_prf full ctxt = Proof_Syntax.pretty_clean_proof_of ctxt full;
   13.57 +
   13.58 +fun pretty_theory ctxt (name, pos) = (Theory.check ctxt (name, pos); Pretty.str name);
   13.59 +
   13.60 +fun basic_entities name scan pretty =
   13.61 +  Document_Antiquotation.setup name scan (fn {source, context = ctxt, ...} =>
   13.62 +    Thy_Output.output ctxt o Thy_Output.maybe_pretty_source pretty ctxt source);
   13.63 +
   13.64 +fun basic_entities_style name scan pretty =
   13.65 +  Document_Antiquotation.setup name scan
   13.66 +    (fn {source, context = ctxt, ...} => fn (style, xs) =>
   13.67 +      Thy_Output.output ctxt
   13.68 +        (Thy_Output.maybe_pretty_source
   13.69 +          (fn ctxt => fn x => pretty ctxt (style, x)) ctxt source xs));
   13.70 +
   13.71 +fun basic_entity name scan = basic_entities name (scan >> single);
   13.72 +
   13.73 +in
   13.74 +
   13.75 +val _ = Theory.setup
   13.76 + (basic_entities_style \<^binding>\<open>thm\<close> (Term_Style.parse -- Attrib.thms) pretty_thm_style #>
   13.77 +  basic_entity \<^binding>\<open>prop\<close> (Term_Style.parse -- Args.prop) pretty_term_style #>
   13.78 +  basic_entity \<^binding>\<open>term\<close> (Term_Style.parse -- Args.term) pretty_term_style #>
   13.79 +  basic_entity \<^binding>\<open>term_type\<close> (Term_Style.parse -- Args.term) pretty_term_typ #>
   13.80 +  basic_entity \<^binding>\<open>typeof\<close> (Term_Style.parse -- Args.term) pretty_term_typeof #>
   13.81 +  basic_entity \<^binding>\<open>const\<close> (Args.const {proper = true, strict = false}) pretty_const #>
   13.82 +  basic_entity \<^binding>\<open>abbrev\<close> (Scan.lift Args.embedded_inner_syntax) pretty_abbrev #>
   13.83 +  basic_entity \<^binding>\<open>typ\<close> Args.typ_abbrev Syntax.pretty_typ #>
   13.84 +  basic_entity \<^binding>\<open>locale\<close> (Scan.lift (Parse.position Args.name)) pretty_locale #>
   13.85 +  basic_entity \<^binding>\<open>class\<close> (Scan.lift Args.embedded_inner_syntax) pretty_class #>
   13.86 +  basic_entity \<^binding>\<open>type\<close> (Scan.lift Args.embedded) pretty_type #>
   13.87 +  basic_entities \<^binding>\<open>prf\<close> Attrib.thms (pretty_prf false) #>
   13.88 +  basic_entities \<^binding>\<open>full_prf\<close> Attrib.thms (pretty_prf true) #>
   13.89 +  basic_entity \<^binding>\<open>theory\<close> (Scan.lift (Parse.position Args.name)) pretty_theory);
   13.90 +
   13.91 +end;
   13.92 +
   13.93 +
   13.94  (* Markdown errors *)
   13.95  
   13.96  local
   13.97  
   13.98  fun markdown_error binding =
   13.99 -  Thy_Output.antiquotation binding (Scan.succeed ())
  13.100 +  Document_Antiquotation.setup binding (Scan.succeed ())
  13.101      (fn {source, ...} => fn _ =>
  13.102        error ("Bad Markdown structure: illegal " ^ quote (Binding.name_of binding) ^
  13.103          Position.here (Position.no_range_position (#1 (Token.range_of source)))))
  13.104 @@ -32,10 +119,14 @@
  13.105  
  13.106  val _ =
  13.107    Theory.setup
  13.108 -   (Thy_Output.antiquotation \<^binding>\<open>noindent\<close> (Scan.succeed ()) (K (K "\\noindent")) #>
  13.109 -    Thy_Output.antiquotation \<^binding>\<open>smallskip\<close> (Scan.succeed ()) (K (K "\\smallskip")) #>
  13.110 -    Thy_Output.antiquotation \<^binding>\<open>medskip\<close> (Scan.succeed ()) (K (K "\\medskip")) #>
  13.111 -    Thy_Output.antiquotation \<^binding>\<open>bigskip\<close> (Scan.succeed ()) (K (K "\\bigskip")));
  13.112 +   (Document_Antiquotation.setup \<^binding>\<open>noindent\<close> (Scan.succeed ())
  13.113 +      (K (K "\\noindent")) #>
  13.114 +    Document_Antiquotation.setup \<^binding>\<open>smallskip\<close> (Scan.succeed ())
  13.115 +      (K (K "\\smallskip")) #>
  13.116 +    Document_Antiquotation.setup \<^binding>\<open>medskip\<close> (Scan.succeed ())
  13.117 +      (K (K "\\medskip")) #>
  13.118 +    Document_Antiquotation.setup \<^binding>\<open>bigskip\<close> (Scan.succeed ())
  13.119 +      (K (K "\\bigskip")));
  13.120  
  13.121  
  13.122  (* control style *)
  13.123 @@ -43,7 +134,7 @@
  13.124  local
  13.125  
  13.126  fun control_antiquotation name s1 s2 =
  13.127 -  Thy_Output.antiquotation name (Scan.lift Args.cartouche_input)
  13.128 +  Document_Antiquotation.setup name (Scan.lift Args.cartouche_input)
  13.129      (fn {context = ctxt, ...} =>
  13.130        enclose s1 s2 o Latex.output_text o Thy_Output.output_text ctxt {markdown = false});
  13.131  
  13.132 @@ -63,7 +154,7 @@
  13.133  local
  13.134  
  13.135  fun text_antiquotation name =
  13.136 -  Thy_Output.antiquotation name (Scan.lift Args.text_input)
  13.137 +  Document_Antiquotation.setup name (Scan.lift Args.text_input)
  13.138      (fn {context = ctxt, ...} => fn source =>
  13.139       (Context_Position.report ctxt (Input.pos_of source)
  13.140          (Markup.language_text (Input.is_delimited source));
  13.141 @@ -83,7 +174,7 @@
  13.142  
  13.143  val _ =
  13.144    Theory.setup
  13.145 -    (Thy_Output.antiquotation \<^binding>\<open>theory_text\<close> (Scan.lift Args.text_input)
  13.146 +    (Document_Antiquotation.setup \<^binding>\<open>theory_text\<close> (Scan.lift Args.text_input)
  13.147        (fn {context = ctxt, ...} => fn source =>
  13.148          let
  13.149            val _ =
  13.150 @@ -93,16 +184,18 @@
  13.151            val keywords = Thy_Header.get_keywords' ctxt;
  13.152            val toks =
  13.153              Input.source_explode source
  13.154 -            |> not (Config.get ctxt Thy_Output.display) ? Symbol_Pos.trim_lines
  13.155 +            |> not (Config.get ctxt Document_Antiquotation.thy_output_display) ?
  13.156 +                Symbol_Pos.trim_lines
  13.157              |> Source.of_list
  13.158              |> Token.source' true keywords
  13.159              |> Source.exhaust;
  13.160            val _ = Context_Position.reports_text ctxt (maps (Token.reports keywords) toks);
  13.161            val indentation =
  13.162 -            Latex.output_symbols (replicate (Config.get ctxt Thy_Output.indent) Symbol.space);
  13.163 +            Latex.output_symbols
  13.164 +              (replicate (Config.get ctxt Document_Antiquotation.thy_output_indent) Symbol.space);
  13.165          in
  13.166            Latex.output_text (maps (Thy_Output.output_token ctxt) toks) |>
  13.167 -           (if Config.get ctxt Thy_Output.display then
  13.168 +           (if Config.get ctxt Document_Antiquotation.thy_output_display then
  13.169                split_lines #> map (prefix indentation) #> cat_lines #>
  13.170                Latex.environment "isabelle"
  13.171              else enclose "\\isa{" "}")
  13.172 @@ -113,7 +206,7 @@
  13.173  
  13.174  local
  13.175  
  13.176 -fun goal_state name main = Thy_Output.antiquotation name (Scan.succeed ())
  13.177 +fun goal_state name main = Document_Antiquotation.setup name (Scan.succeed ())
  13.178    (fn {context = ctxt, ...} => fn () =>
  13.179      Thy_Output.output ctxt
  13.180        [Goal_Display.pretty_goal
  13.181 @@ -132,7 +225,7 @@
  13.182  (* embedded lemma *)
  13.183  
  13.184  val _ = Theory.setup
  13.185 -  (Thy_Output.antiquotation \<^binding>\<open>lemma\<close>
  13.186 +  (Document_Antiquotation.setup \<^binding>\<open>lemma\<close>
  13.187      (Scan.lift (Scan.ahead Parse.not_eof) -- Args.prop --
  13.188        Scan.lift (Parse.position (Parse.reserved "by") -- Method.parse -- Scan.option Method.parse))
  13.189      (fn {source, context = ctxt, ...} => fn ((prop_token, prop), (((_, by_pos), m1), m2)) =>
  13.190 @@ -157,7 +250,7 @@
  13.191  
  13.192  val _ =
  13.193    Theory.setup
  13.194 -    (Thy_Output.antiquotation \<^binding>\<open>verbatim\<close> (Scan.lift Args.text_input)
  13.195 +    (Document_Antiquotation.setup \<^binding>\<open>verbatim\<close> (Scan.lift Args.text_input)
  13.196        (fn {context = ctxt, ...} => fn source =>
  13.197         (Context_Position.report ctxt (Input.pos_of source)
  13.198            (Markup.language_verbatim (Input.is_delimited source));
  13.199 @@ -168,7 +261,7 @@
  13.200  
  13.201  local
  13.202  
  13.203 -fun ml_text name ml = Thy_Output.antiquotation name (Scan.lift Args.text_input)
  13.204 +fun ml_text name ml = Document_Antiquotation.setup name (Scan.lift Args.text_input)
  13.205    (fn {context = ctxt, ...} => fn source =>
  13.206     (ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (Input.pos_of source) (ml source);
  13.207      Thy_Output.verbatim_text ctxt (Input.source_content source)));
  13.208 @@ -198,7 +291,7 @@
  13.209  (* URLs *)
  13.210  
  13.211  val _ = Theory.setup
  13.212 -  (Thy_Output.antiquotation \<^binding>\<open>url\<close> (Scan.lift (Parse.position Parse.embedded))
  13.213 +  (Document_Antiquotation.setup \<^binding>\<open>url\<close> (Scan.lift (Parse.position Parse.embedded))
  13.214      (fn {context = ctxt, ...} => fn (name, pos) =>
  13.215        (Context_Position.reports ctxt [(pos, Markup.language_path), (pos, Markup.url name)];
  13.216         enclose "\\url{" "}" name)));
  13.217 @@ -207,7 +300,7 @@
  13.218  (* doc entries *)
  13.219  
  13.220  val _ = Theory.setup
  13.221 -  (Thy_Output.antiquotation \<^binding>\<open>doc\<close> (Scan.lift (Parse.position Parse.embedded))
  13.222 +  (Document_Antiquotation.setup \<^binding>\<open>doc\<close> (Scan.lift (Parse.position Parse.embedded))
  13.223      (fn {context = ctxt, ...} => fn (name, pos) =>
  13.224        (Context_Position.report ctxt pos (Markup.doc name);
  13.225          Thy_Output.output ctxt [Thy_Output.pretty_text ctxt name])));
  13.226 @@ -216,7 +309,7 @@
  13.227  (* formal entities *)
  13.228  
  13.229  fun entity_antiquotation name check output =
  13.230 -  Thy_Output.antiquotation name (Scan.lift (Parse.position Args.name))
  13.231 +  Document_Antiquotation.setup name (Scan.lift (Parse.position Args.name))
  13.232      (fn {context = ctxt, ...} => fn (name, pos) => (check ctxt (name, pos); output name));
  13.233  
  13.234  val _ =
    14.1 --- a/src/Pure/Thy/thy_output.ML	Tue Jan 09 15:18:41 2018 +0100
    14.2 +++ b/src/Pure/Thy/thy_output.ML	Tue Jan 09 15:40:12 2018 +0100
    14.3 @@ -1,28 +1,11 @@
    14.4  (*  Title:      Pure/Thy/thy_output.ML
    14.5 -    Author:     Markus Wenzel, TU Muenchen
    14.6 +    Author:     Makarius
    14.7  
    14.8 -Theory document output with antiquotations.
    14.9 +Theory document output.
   14.10  *)
   14.11  
   14.12  signature THY_OUTPUT =
   14.13  sig
   14.14 -  val display: bool Config.T
   14.15 -  val quotes: bool Config.T
   14.16 -  val margin: int Config.T
   14.17 -  val indent: int Config.T
   14.18 -  val source: bool Config.T
   14.19 -  val break: bool Config.T
   14.20 -  val modes: string Config.T
   14.21 -  val add_wrapper: ((unit -> string) -> unit -> string) -> Proof.context -> Proof.context
   14.22 -  val add_option: binding -> (string -> Proof.context -> Proof.context) -> theory -> theory
   14.23 -  val check_command: Proof.context -> xstring * Position.T -> string
   14.24 -  val check_option: Proof.context -> xstring * Position.T -> string
   14.25 -  val print_antiquotations: bool -> Proof.context -> unit
   14.26 -  val antiquotation: binding -> 'a context_parser ->
   14.27 -    ({source: Token.src, context: Proof.context} -> 'a -> string) -> theory -> theory
   14.28 -  val boolean: string -> bool
   14.29 -  val integer: string -> int
   14.30 -  val eval_antiquote: Proof.context -> Antiquote.text_antiquote -> string
   14.31    val output_text: Proof.context -> {markdown: bool} -> Input.source -> Latex.text list
   14.32    val check_comments: Proof.context -> Symbol_Pos.T list -> unit
   14.33    val check_token_comments: Proof.context -> Token.T -> unit
   14.34 @@ -43,152 +26,6 @@
   14.35  structure Thy_Output: THY_OUTPUT =
   14.36  struct
   14.37  
   14.38 -(** options **)
   14.39 -
   14.40 -val display = Attrib.setup_option_bool ("thy_output_display", \<^here>);
   14.41 -val break = Attrib.setup_option_bool ("thy_output_break", \<^here>);
   14.42 -val quotes = Attrib.setup_option_bool ("thy_output_quotes", \<^here>);
   14.43 -val margin = Attrib.setup_option_int ("thy_output_margin", \<^here>);
   14.44 -val indent = Attrib.setup_option_int ("thy_output_indent", \<^here>);
   14.45 -val source = Attrib.setup_option_bool ("thy_output_source", \<^here>);
   14.46 -val modes = Attrib.setup_option_string ("thy_output_modes", \<^here>);
   14.47 -
   14.48 -
   14.49 -structure Wrappers = Proof_Data
   14.50 -(
   14.51 -  type T = ((unit -> string) -> unit -> string) list;
   14.52 -  fun init _ = [];
   14.53 -);
   14.54 -
   14.55 -fun add_wrapper wrapper = Wrappers.map (cons wrapper);
   14.56 -
   14.57 -val wrap = Wrappers.get #> fold (fn wrapper => fn f => wrapper f);
   14.58 -
   14.59 -
   14.60 -
   14.61 -(** maintain global antiquotations **)
   14.62 -
   14.63 -structure Antiquotations = Theory_Data
   14.64 -(
   14.65 -  type T =
   14.66 -    (Token.src -> Proof.context -> string) Name_Space.table *
   14.67 -      (string -> Proof.context -> Proof.context) Name_Space.table;
   14.68 -  val empty : T =
   14.69 -    (Name_Space.empty_table Markup.document_antiquotationN,
   14.70 -      Name_Space.empty_table Markup.document_antiquotation_optionN);
   14.71 -  val extend = I;
   14.72 -  fun merge ((commands1, options1), (commands2, options2)) : T =
   14.73 -    (Name_Space.merge_tables (commands1, commands2),
   14.74 -      Name_Space.merge_tables (options1, options2));
   14.75 -);
   14.76 -
   14.77 -val get_antiquotations = Antiquotations.get o Proof_Context.theory_of;
   14.78 -
   14.79 -fun add_command name cmd thy = thy
   14.80 -  |> Antiquotations.map (apfst (Name_Space.define (Context.Theory thy) true (name, cmd) #> snd));
   14.81 -
   14.82 -fun add_option name opt thy = thy
   14.83 -  |> Antiquotations.map (apsnd (Name_Space.define (Context.Theory thy) true (name, opt) #> snd));
   14.84 -
   14.85 -fun check_command ctxt = #1 o Name_Space.check (Context.Proof ctxt) (#1 (get_antiquotations ctxt));
   14.86 -
   14.87 -fun check_option ctxt = #1 o Name_Space.check (Context.Proof ctxt) (#2 (get_antiquotations ctxt));
   14.88 -
   14.89 -fun command src ctxt =
   14.90 -  let val (src', f) = Token.check_src ctxt (#1 o get_antiquotations) src
   14.91 -  in f src' ctxt end;
   14.92 -
   14.93 -fun option ((xname, pos), s) ctxt =
   14.94 -  let
   14.95 -    val (_, opt) =
   14.96 -      Name_Space.check (Context.Proof ctxt) (#2 (get_antiquotations ctxt)) (xname, pos);
   14.97 -  in opt s ctxt end;
   14.98 -
   14.99 -fun print_antiquotations verbose ctxt =
  14.100 -  let
  14.101 -    val (commands, options) = get_antiquotations ctxt;
  14.102 -    val command_names = map #1 (Name_Space.markup_table verbose ctxt commands);
  14.103 -    val option_names = map #1 (Name_Space.markup_table verbose ctxt options);
  14.104 -  in
  14.105 -    [Pretty.big_list "document antiquotations:" (map Pretty.mark_str command_names),
  14.106 -     Pretty.big_list "document antiquotation options:" (map Pretty.mark_str option_names)]
  14.107 -  end |> Pretty.writeln_chunks;
  14.108 -
  14.109 -fun antiquotation name scan body =
  14.110 -  add_command name
  14.111 -    (fn src => fn ctxt =>
  14.112 -      let val (x, ctxt') = Token.syntax scan src ctxt
  14.113 -      in body {source = src, context = ctxt'} x end);
  14.114 -
  14.115 -
  14.116 -
  14.117 -(** syntax of antiquotations **)
  14.118 -
  14.119 -(* option values *)
  14.120 -
  14.121 -fun boolean "" = true
  14.122 -  | boolean "true" = true
  14.123 -  | boolean "false" = false
  14.124 -  | boolean s = error ("Bad boolean value: " ^ quote s);
  14.125 -
  14.126 -fun integer s =
  14.127 -  let
  14.128 -    fun int ss =
  14.129 -      (case Library.read_int ss of (i, []) => i
  14.130 -      | _ => error ("Bad integer value: " ^ quote s));
  14.131 -  in (case Symbol.explode s of "-" :: ss => ~ (int ss) | ss => int ss) end;
  14.132 -
  14.133 -
  14.134 -(* outer syntax *)
  14.135 -
  14.136 -local
  14.137 -
  14.138 -val property =
  14.139 -  Parse.position Parse.name -- Scan.optional (Parse.$$$ "=" |-- Parse.!!! Parse.name) "";
  14.140 -
  14.141 -val properties =
  14.142 -  Scan.optional (Parse.$$$ "[" |-- Parse.!!! (Parse.enum "," property --| Parse.$$$ "]")) [];
  14.143 -
  14.144 -in
  14.145 -
  14.146 -val antiq =
  14.147 -  Parse.!!!
  14.148 -    (Parse.token Parse.liberal_name -- properties -- Parse.args --| Scan.ahead Parse.eof)
  14.149 -  >> (fn ((name, props), args) => (props, name :: args));
  14.150 -
  14.151 -end;
  14.152 -
  14.153 -
  14.154 -(* eval antiquote *)
  14.155 -
  14.156 -local
  14.157 -
  14.158 -fun eval_antiq ctxt (opts, src) =
  14.159 -  let
  14.160 -    val preview_ctxt = fold option opts ctxt;
  14.161 -    val print_ctxt = Context_Position.set_visible false preview_ctxt;
  14.162 -
  14.163 -    fun cmd ctxt = wrap ctxt (fn () => command src ctxt) ();
  14.164 -    val _ = cmd preview_ctxt;
  14.165 -    val print_modes = space_explode "," (Config.get print_ctxt modes) @ [Latex.latexN];
  14.166 -  in Print_Mode.with_modes print_modes (fn () => cmd print_ctxt) () end;
  14.167 -
  14.168 -in
  14.169 -
  14.170 -fun eval_antiquote _ (Antiquote.Text ss) = Symbol_Pos.content ss
  14.171 -  | eval_antiquote ctxt (Antiquote.Control {name, body, ...}) =
  14.172 -      eval_antiq ctxt
  14.173 -        ([], Token.make_src name (if null body then [] else [Token.read_cartouche body]))
  14.174 -  | eval_antiquote ctxt (Antiquote.Antiq {range = (pos, _), body, ...}) =
  14.175 -      let val keywords = Thy_Header.get_keywords' ctxt;
  14.176 -      in eval_antiq ctxt (Token.read_antiq keywords antiq (body, pos)) end;
  14.177 -
  14.178 -end;
  14.179 -
  14.180 -
  14.181 -
  14.182 -(** document output **)
  14.183 -
  14.184  (* output text *)
  14.185  
  14.186  fun output_text ctxt {markdown} source =
  14.187 @@ -199,7 +36,8 @@
  14.188      val _ = Context_Position.report ctxt pos (Markup.language_document (Input.is_delimited source));
  14.189  
  14.190      val output_antiquotes =
  14.191 -      map (fn ant => Latex.text (eval_antiquote ctxt ant, #1 (Antiquote.range [ant])));
  14.192 +      map (fn ant =>
  14.193 +        Latex.text (Document_Antiquotation.evaluate ctxt ant, #1 (Antiquote.range [ant])));
  14.194  
  14.195      fun output_line line =
  14.196        (if Markdown.line_is_item line then [Latex.string "\\item "] else []) @
  14.197 @@ -572,34 +410,12 @@
  14.198  
  14.199  
  14.200  
  14.201 -(** setup default output **)
  14.202 -
  14.203 -(* options *)
  14.204 -
  14.205 -val _ = Theory.setup
  14.206 - (add_option \<^binding>\<open>show_types\<close> (Config.put show_types o boolean) #>
  14.207 -  add_option \<^binding>\<open>show_sorts\<close> (Config.put show_sorts o boolean) #>
  14.208 -  add_option \<^binding>\<open>show_structs\<close> (Config.put show_structs o boolean) #>
  14.209 -  add_option \<^binding>\<open>show_question_marks\<close> (Config.put show_question_marks o boolean) #>
  14.210 -  add_option \<^binding>\<open>show_abbrevs\<close> (Config.put show_abbrevs o boolean) #>
  14.211 -  add_option \<^binding>\<open>names_long\<close> (Config.put Name_Space.names_long o boolean) #>
  14.212 -  add_option \<^binding>\<open>names_short\<close> (Config.put Name_Space.names_short o boolean) #>
  14.213 -  add_option \<^binding>\<open>names_unique\<close> (Config.put Name_Space.names_unique o boolean) #>
  14.214 -  add_option \<^binding>\<open>eta_contract\<close> (Config.put Syntax_Trans.eta_contract o boolean) #>
  14.215 -  add_option \<^binding>\<open>display\<close> (Config.put display o boolean) #>
  14.216 -  add_option \<^binding>\<open>break\<close> (Config.put break o boolean) #>
  14.217 -  add_option \<^binding>\<open>quotes\<close> (Config.put quotes o boolean) #>
  14.218 -  add_option \<^binding>\<open>mode\<close> (add_wrapper o Print_Mode.with_modes o single) #>
  14.219 -  add_option \<^binding>\<open>margin\<close> (Config.put margin o integer) #>
  14.220 -  add_option \<^binding>\<open>indent\<close> (Config.put indent o integer) #>
  14.221 -  add_option \<^binding>\<open>source\<close> (Config.put source o boolean) #>
  14.222 -  add_option \<^binding>\<open>goals_limit\<close> (Config.put Goal_Display.goals_limit o integer));
  14.223 -
  14.224 +(** standard output operations **)
  14.225  
  14.226  (* basic pretty printing *)
  14.227  
  14.228  fun perhaps_trim ctxt =
  14.229 -  not (Config.get ctxt display) ? Symbol.trim_blanks;
  14.230 +  not (Config.get ctxt Document_Antiquotation.thy_output_display) ? Symbol.trim_blanks;
  14.231  
  14.232  fun pretty_text ctxt =
  14.233    Pretty.chunks o map Pretty.str o map (perhaps_trim ctxt) o split_lines;
  14.234 @@ -608,55 +424,6 @@
  14.235  
  14.236  fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of;
  14.237  
  14.238 -fun pretty_term_style ctxt (style, t) =
  14.239 -  pretty_term ctxt (style t);
  14.240 -
  14.241 -fun pretty_thm_style ctxt (style, th) =
  14.242 -  pretty_term ctxt (style (Thm.full_prop_of th));
  14.243 -
  14.244 -fun pretty_term_typ ctxt (style, t) =
  14.245 -  let val t' = style t
  14.246 -  in pretty_term ctxt (Type.constraint (Term.fastype_of t') t') end;
  14.247 -
  14.248 -fun pretty_term_typeof ctxt (style, t) =
  14.249 -  Syntax.pretty_typ ctxt (Term.fastype_of (style t));
  14.250 -
  14.251 -fun pretty_const ctxt c =
  14.252 -  let
  14.253 -    val t = Const (c, Consts.type_scheme (Proof_Context.consts_of ctxt) c)
  14.254 -      handle TYPE (msg, _, _) => error msg;
  14.255 -    val ([t'], _) = Variable.import_terms true [t] ctxt;
  14.256 -  in pretty_term ctxt t' end;
  14.257 -
  14.258 -fun pretty_abbrev ctxt s =
  14.259 -  let
  14.260 -    val t = Syntax.read_term (Proof_Context.set_mode Proof_Context.mode_abbrev ctxt) s;
  14.261 -    fun err () = error ("Abbreviated constant expected: " ^ Syntax.string_of_term ctxt t);
  14.262 -    val (head, args) = Term.strip_comb t;
  14.263 -    val (c, T) = Term.dest_Const head handle TERM _ => err ();
  14.264 -    val (U, u) = Consts.the_abbreviation (Proof_Context.consts_of ctxt) c
  14.265 -      handle TYPE _ => err ();
  14.266 -    val t' = Term.betapplys (Envir.expand_atom T (U, u), args);
  14.267 -    val eq = Logic.mk_equals (t, t');
  14.268 -    val ctxt' = Variable.auto_fixes eq ctxt;
  14.269 -  in Proof_Context.pretty_term_abbrev ctxt' eq end;
  14.270 -
  14.271 -fun pretty_locale ctxt (name, pos) =
  14.272 -  let
  14.273 -    val thy = Proof_Context.theory_of ctxt
  14.274 -  in (Pretty.str o Locale.extern thy o Locale.check thy) (name, pos) end;
  14.275 -
  14.276 -fun pretty_class ctxt =
  14.277 -  Pretty.str o Proof_Context.extern_class ctxt o Proof_Context.read_class ctxt;
  14.278 -
  14.279 -fun pretty_type ctxt s =
  14.280 -  let val Type (name, _) = Proof_Context.read_type_name {proper = true, strict = false} ctxt s
  14.281 -  in Pretty.str (Proof_Context.extern_type ctxt name) end;
  14.282 -
  14.283 -fun pretty_prf full ctxt = Proof_Syntax.pretty_clean_proof_of ctxt full;
  14.284 -
  14.285 -fun pretty_theory ctxt (name, pos) = (Theory.check ctxt (name, pos); Pretty.str name);
  14.286 -
  14.287  
  14.288  (* default output *)
  14.289  
  14.290 @@ -664,21 +431,24 @@
  14.291  
  14.292  fun maybe_pretty_source pretty ctxt src xs =
  14.293    map (pretty ctxt) xs  (*always pretty in order to exhibit errors!*)
  14.294 -  |> (if Config.get ctxt source then K [pretty_text ctxt (str_of_source src)] else I);
  14.295 +  |> (if Config.get ctxt Document_Antiquotation.thy_output_source
  14.296 +      then K [pretty_text ctxt (str_of_source src)] else I);
  14.297  
  14.298 -fun string_of_margin ctxt = Pretty.string_of_margin (Config.get ctxt margin);
  14.299 +fun string_of_margin ctxt =
  14.300 +  Pretty.string_of_margin (Config.get ctxt Document_Antiquotation.thy_output_margin);
  14.301  
  14.302  fun output ctxt prts =
  14.303    prts
  14.304 -  |> Config.get ctxt quotes ? map Pretty.quote
  14.305 -  |> (if Config.get ctxt display then
  14.306 -        map (Pretty.indent (Config.get ctxt indent) #> string_of_margin ctxt #> Output.output)
  14.307 +  |> Config.get ctxt Document_Antiquotation.thy_output_quotes ? map Pretty.quote
  14.308 +  |> (if Config.get ctxt Document_Antiquotation.thy_output_display then
  14.309 +        map (Pretty.indent (Config.get ctxt Document_Antiquotation.thy_output_indent)
  14.310 +          #> string_of_margin ctxt #> Output.output)
  14.311          #> space_implode "\\isasep\\isanewline%\n"
  14.312          #> Latex.environment "isabelle"
  14.313        else
  14.314          map
  14.315 -          ((if Config.get ctxt break then string_of_margin ctxt else Pretty.unformatted_string_of)
  14.316 -            #> Output.output)
  14.317 +          ((if Config.get ctxt Document_Antiquotation.thy_output_break
  14.318 +            then string_of_margin ctxt else Pretty.unformatted_string_of) #> Output.output)
  14.319          #> space_implode "\\isasep\\isanewline%\n"
  14.320          #> enclose "\\isa{" "}");
  14.321  
  14.322 @@ -686,48 +456,14 @@
  14.323  (* verbatim text *)
  14.324  
  14.325  fun verbatim_text ctxt =
  14.326 -  if Config.get ctxt display then
  14.327 -    split_lines #> map (prefix (Symbol.spaces (Config.get ctxt indent))) #> cat_lines #>
  14.328 +  if Config.get ctxt Document_Antiquotation.thy_output_display then
  14.329 +    split_lines #>
  14.330 +    map (prefix (Symbol.spaces (Config.get ctxt Document_Antiquotation.thy_output_indent))) #>
  14.331 +    cat_lines #>
  14.332      Latex.output_ascii #> Latex.environment "isabellett"
  14.333    else
  14.334      split_lines #>
  14.335      map (Latex.output_ascii #> enclose "\\isatt{" "}") #>
  14.336      space_implode "\\isasep\\isanewline%\n";
  14.337  
  14.338 -
  14.339 -(* antiquotations for basic entities *)
  14.340 -
  14.341 -local
  14.342 -
  14.343 -fun basic_entities name scan pretty =
  14.344 -  antiquotation name scan (fn {source, context = ctxt, ...} =>
  14.345 -    output ctxt o maybe_pretty_source pretty ctxt source);
  14.346 -
  14.347 -fun basic_entities_style name scan pretty =
  14.348 -  antiquotation name scan (fn {source, context = ctxt, ...} => fn (style, xs) =>
  14.349 -    output ctxt
  14.350 -      (maybe_pretty_source (fn ctxt => fn x => pretty ctxt (style, x)) ctxt source xs));
  14.351 -
  14.352 -fun basic_entity name scan = basic_entities name (scan >> single);
  14.353 -
  14.354 -in
  14.355 -
  14.356 -val _ = Theory.setup
  14.357 - (basic_entities_style \<^binding>\<open>thm\<close> (Term_Style.parse -- Attrib.thms) pretty_thm_style #>
  14.358 -  basic_entity \<^binding>\<open>prop\<close> (Term_Style.parse -- Args.prop) pretty_term_style #>
  14.359 -  basic_entity \<^binding>\<open>term\<close> (Term_Style.parse -- Args.term) pretty_term_style #>
  14.360 -  basic_entity \<^binding>\<open>term_type\<close> (Term_Style.parse -- Args.term) pretty_term_typ #>
  14.361 -  basic_entity \<^binding>\<open>typeof\<close> (Term_Style.parse -- Args.term) pretty_term_typeof #>
  14.362 -  basic_entity \<^binding>\<open>const\<close> (Args.const {proper = true, strict = false}) pretty_const #>
  14.363 -  basic_entity \<^binding>\<open>abbrev\<close> (Scan.lift Args.embedded_inner_syntax) pretty_abbrev #>
  14.364 -  basic_entity \<^binding>\<open>typ\<close> Args.typ_abbrev Syntax.pretty_typ #>
  14.365 -  basic_entity \<^binding>\<open>locale\<close> (Scan.lift (Parse.position Args.name)) pretty_locale #>
  14.366 -  basic_entity \<^binding>\<open>class\<close> (Scan.lift Args.embedded_inner_syntax) pretty_class #>
  14.367 -  basic_entity \<^binding>\<open>type\<close> (Scan.lift Args.embedded) pretty_type #>
  14.368 -  basic_entities \<^binding>\<open>prf\<close> Attrib.thms (pretty_prf false) #>
  14.369 -  basic_entities \<^binding>\<open>full_prf\<close> Attrib.thms (pretty_prf true) #>
  14.370 -  basic_entity \<^binding>\<open>theory\<close> (Scan.lift (Parse.position Args.name)) pretty_theory);
  14.371 -
  14.372  end;
  14.373 -
  14.374 -end;
    15.1 --- a/src/Pure/Tools/jedit.ML	Tue Jan 09 15:18:41 2018 +0100
    15.2 +++ b/src/Pure/Tools/jedit.ML	Tue Jan 09 15:40:12 2018 +0100
    15.3 @@ -75,7 +75,7 @@
    15.4  
    15.5  val _ =
    15.6    Theory.setup
    15.7 -    (Thy_Output.antiquotation \<^binding>\<open>action\<close> (Scan.lift (Parse.position Parse.embedded))
    15.8 +    (Document_Antiquotation.setup \<^binding>\<open>action\<close> (Scan.lift (Parse.position Parse.embedded))
    15.9        (fn {context = ctxt, ...} => fn (name, pos) =>
   15.10         (if Context_Position.is_reported ctxt pos then ignore (check_action (name, pos)) else ();
   15.11          Thy_Output.verbatim_text ctxt name)));
    16.1 --- a/src/Pure/Tools/rail.ML	Tue Jan 09 15:18:41 2018 +0100
    16.2 +++ b/src/Pure/Tools/rail.ML	Tue Jan 09 15:40:12 2018 +0100
    16.3 @@ -332,7 +332,7 @@
    16.4  
    16.5  fun output_rules ctxt rules =
    16.6    let
    16.7 -    val output_antiq = Thy_Output.eval_antiquote ctxt o Antiquote.Antiq;
    16.8 +    val output_antiq = Document_Antiquotation.evaluate ctxt o Antiquote.Antiq;
    16.9      fun output_text b s =
   16.10        Output.output s
   16.11        |> b ? enclose "\\isakeyword{" "}"
   16.12 @@ -374,7 +374,7 @@
   16.13    in Latex.environment "railoutput" (implode (map output_rule rules)) end;
   16.14  
   16.15  val _ = Theory.setup
   16.16 -  (Thy_Output.antiquotation \<^binding>\<open>rail\<close> (Scan.lift Args.text_input)
   16.17 +  (Document_Antiquotation.setup \<^binding>\<open>rail\<close> (Scan.lift Args.text_input)
   16.18      (fn {context = ctxt, ...} => output_rules ctxt o read ctxt));
   16.19  
   16.20  end;
    17.1 --- a/src/Tools/Code/code_target.ML	Tue Jan 09 15:18:41 2018 +0100
    17.2 +++ b/src/Tools/Code/code_target.ML	Tue Jan 09 15:40:12 2018 +0100
    17.3 @@ -510,7 +510,7 @@
    17.4  in
    17.5  
    17.6  val _ = Theory.setup
    17.7 -  (Thy_Output.antiquotation @{binding code_stmts}
    17.8 +  (Document_Antiquotation.setup @{binding code_stmts}
    17.9      (parse_const_terms --
   17.10        Scan.repeat (parse_consts || parse_types || parse_classes || parse_instances)
   17.11        -- Scan.lift (Args.parens (Args.name -- Scan.option Parse.int)))