# HG changeset patch
# User wenzelm
# Date 1515453432 -3600
# Node ID aacea75450b4b4968050244c8e540aad3b9c98cb
# Parent  39e4668ded4f1b593121ac63da0d284507989f5c# Parent  2d9cf74943e14bf732909f21006ff74563248ffc
merged;

diff -r 2d9cf74943e1 -r aacea75450b4 NEWS
--- a/NEWS	Mon Jan 08 17:11:25 2018 +0000
+++ b/NEWS	Tue Jan 09 00:17:12 2018 +0100
@@ -108,6 +108,10 @@
 syntax, antiquotations are interpreted wrt. the presentation context of
 the enclosing command.
 
+* Outside of the inner theory body, the default presentation context is
+theory Pure. Thus elementary antiquotations may be used in markup
+commands (e.g. 'chapter', 'section', 'text') and formal comments.
+
 * System option "document_tags" specifies a default for otherwise
 untagged commands. This is occasionally useful to control the global
 visibility of commands via session options (e.g. in ROOT).
diff -r 2d9cf74943e1 -r aacea75450b4 lib/texinputs/isabelle.sty
--- a/lib/texinputs/isabelle.sty	Mon Jan 08 17:11:25 2018 +0000
+++ b/lib/texinputs/isabelle.sty	Tue Jan 09 00:17:12 2018 +0100
@@ -39,7 +39,6 @@
 \DeclareRobustCommand{\isactrlesup}{\egroup\egroup\endmath\egroup}
 \newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}
 
-\newcommand{\isaantiqcontrol}[1]{\isatt{{\char`\\}{\char`\<}{\char`\^}#1{\char`\>}}}
 \newenvironment{isaantiq}{{\isacharat\isacharbraceleft}}{{\isacharbraceright}}
 
 \newdimen\isa@parindent\newdimen\isa@parskip
diff -r 2d9cf74943e1 -r aacea75450b4 src/HOL/Tools/Metis/metis_reconstruct.ML
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Mon Jan 08 17:11:25 2018 +0000
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Tue Jan 09 00:17:12 2018 +0100
@@ -73,9 +73,9 @@
   let
     val ts = map (hol_term_of_metis ctxt type_enc sym_tab) fol_tms
     val _ = trace_msg ctxt (fn () => "  calling type inference:")
-    val _ = app (fn t => trace_msg ctxt (fn () => Syntax.string_of_term ctxt t)) ts
+    val _ = List.app (fn t => trace_msg ctxt (fn () => Syntax.string_of_term ctxt t)) ts
     val ts' = ts |> polish_hol_terms ctxt concealed
-    val _ = app (fn t => trace_msg ctxt
+    val _ = List.app (fn t => trace_msg ctxt
                   (fn () => "  final term: " ^ Syntax.string_of_term ctxt t ^
                             " of type " ^ Syntax.string_of_typ ctxt (type_of t))) ts'
   in ts' end
diff -r 2d9cf74943e1 -r aacea75450b4 src/HOL/Tools/Metis/metis_tactic.ML
--- a/src/HOL/Tools/Metis/metis_tactic.ML	Mon Jan 08 17:11:25 2018 +0000
+++ b/src/HOL/Tools/Metis/metis_tactic.ML	Tue Jan 09 00:17:12 2018 +0100
@@ -162,7 +162,7 @@
       val dischargers = map (fst o snd) th_cls_pairs
       val cls = cls |> map (Drule.eta_contraction_rule #> do_lams)
       val _ = trace_msg ctxt (K "FOL_SOLVE: CONJECTURE CLAUSES")
-      val _ = app (fn th => trace_msg ctxt (fn () => Thm.string_of_thm ctxt th)) cls
+      val _ = List.app (fn th => trace_msg ctxt (fn () => Thm.string_of_thm ctxt th)) cls
       val _ = trace_msg ctxt (fn () => "type_enc = " ^ type_enc)
       val type_enc = type_enc_of_string Strict type_enc
       val (sym_tab, axioms, ord_info, concealed) =
@@ -174,9 +174,9 @@
         | get_isa_thm _ (Isa_Raw ith) = ith
       val axioms = axioms |> map (fn (mth, ith) => (mth, get_isa_thm mth ith))
       val _ = trace_msg ctxt (K "ISABELLE CLAUSES")
-      val _ = app (fn (_, ith) => trace_msg ctxt (fn () => Thm.string_of_thm ctxt ith)) axioms
+      val _ = List.app (fn (_, ith) => trace_msg ctxt (fn () => Thm.string_of_thm ctxt ith)) axioms
       val _ = trace_msg ctxt (K "METIS CLAUSES")
-      val _ = app (fn (mth, _) => trace_msg ctxt (fn () => Metis_Thm.toString mth)) axioms
+      val _ = List.app (fn (mth, _) => trace_msg ctxt (fn () => Metis_Thm.toString mth)) axioms
       val _ = trace_msg ctxt (K "START METIS PROVE PROCESS")
       val ordering =
         if Config.get ctxt advisory_simp then
@@ -202,7 +202,7 @@
          val result = fold (replay_one_inference ctxt' type_enc concealed sym_tab) proof axioms
          val used = map_filter (used_axioms axioms) proof
          val _ = trace_msg ctxt (K "METIS COMPLETED; clauses actually used:")
-         val _ = app (fn th => trace_msg ctxt (fn () => Thm.string_of_thm ctxt th)) used
+         val _ = List.app (fn th => trace_msg ctxt (fn () => Thm.string_of_thm ctxt th)) used
          val (used_th_cls_pairs, unused_th_cls_pairs) =
            List.partition (have_common_thm ctxt used o snd o snd) th_cls_pairs
          val unused_ths = maps (snd o snd) unused_th_cls_pairs
diff -r 2d9cf74943e1 -r aacea75450b4 src/HOL/ex/Cartouche_Examples.thy
--- a/src/HOL/ex/Cartouche_Examples.thy	Mon Jan 08 17:11:25 2018 +0000
+++ b/src/HOL/ex/Cartouche_Examples.thy	Tue Jan 09 00:17:12 2018 +0100
@@ -141,7 +141,7 @@
   Outer_Syntax.command
     @{command_keyword text_cartouche} ""
     (Parse.opt_target -- Parse.input Parse.cartouche
-      >> Thy_Output.document_command {markdown = true})
+      >> Pure_Syn.document_command {markdown = true})
 \<close>
 
 text_cartouche
diff -r 2d9cf74943e1 -r aacea75450b4 src/Provers/order.ML
--- a/src/Provers/order.ML	Mon Jan 08 17:11:25 2018 +0000
+++ b/src/Provers/order.ML	Tue Jan 09 00:17:12 2018 +0100
@@ -687,7 +687,7 @@
   (* DFS on the graph; apply dfs_visit to each vertex in
      the graph, checking first to make sure the vertex is
      as yet unvisited. *)
-  app (fn u => if been_visited u then ()
+  List.app (fn u => if been_visited u then ()
         else (dfs_visit G u; ()))  (members G);
   visited := [];
 
@@ -765,7 +765,7 @@
     fun update (x,l) = let val _ = pred := (x,l) ::(!pred) in () end;
 
     in if been_visited v then ()
-    else (app (fn (v',l) => if been_visited v' then () else (
+    else (List.app (fn (v',l) => if been_visited v' then () else (
        update (v',l);
        dfs_visit v'; ()) )) (adjacent eq_comp g u')
      end
diff -r 2d9cf74943e1 -r aacea75450b4 src/Provers/quasi.ML
--- a/src/Provers/quasi.ML	Mon Jan 08 17:11:25 2018 +0000
+++ b/src/Provers/quasi.ML	Tue Jan 09 00:17:12 2018 +0100
@@ -361,7 +361,7 @@
     fun update (x,l) = let val _ = pred := (x,l) ::(!pred) in () end;
 
     in if been_visited v then ()
-    else (app (fn (v',l) => if been_visited v' then () else (
+    else (List.app (fn (v',l) => if been_visited v' then () else (
        update (v',l);
        dfs_visit v'; ()) )) (adjacent eq_comp g u')
      end
diff -r 2d9cf74943e1 -r aacea75450b4 src/Provers/trancl.ML
--- a/src/Provers/trancl.ML	Mon Jan 08 17:11:25 2018 +0000
+++ b/src/Provers/trancl.ML	Tue Jan 09 00:17:12 2018 +0100
@@ -287,7 +287,7 @@
     fun update (x,l) = let val _ = pred := (x,l) ::(!pred) in () end;
 
     in if been_visited v then ()
-    else (app (fn (v',l) => if been_visited v' then () else (
+    else (List.app (fn (v',l) => if been_visited v' then () else (
        update (v',l);
        dfs_visit v'; ()) )) (adjacent eq_comp g u')
      end
diff -r 2d9cf74943e1 -r aacea75450b4 src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Mon Jan 08 17:11:25 2018 +0000
+++ b/src/Pure/General/symbol.ML	Tue Jan 09 00:17:12 2018 +0100
@@ -45,6 +45,7 @@
   datatype sym =
     Char of string | UTF8 of string | Sym of string | Control of string | Malformed of string | EOF
   val decode: symbol -> sym
+  val encode: sym -> symbol
   datatype kind = Letter | Digit | Quasi | Blank | Other
   val kind: symbol -> kind
   val is_letter: symbol -> bool
@@ -211,6 +212,13 @@
   else if is_control s then Control (String.substring (s, 3, size s - 4))
   else Sym (String.substring (s, 2, size s - 3));
 
+fun encode (Char s) = s
+  | encode (UTF8 s) = s
+  | encode (Sym s) = "\092<" ^ s ^ ">"
+  | encode (Control s) = "\092<^" ^ s ^ ">"
+  | encode (Malformed s) = s
+  | encode EOF = "";
+
 
 (* standard symbol kinds *)
 
diff -r 2d9cf74943e1 -r aacea75450b4 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Mon Jan 08 17:11:25 2018 +0000
+++ b/src/Pure/Isar/toplevel.ML	Tue Jan 09 00:17:12 2018 +0100
@@ -8,6 +8,7 @@
 sig
   exception UNDEF
   type state
+  val generic_theory_toplevel: generic_theory -> state
   val theory_toplevel: theory -> state
   val toplevel: state
   val is_toplevel: state -> bool
@@ -15,7 +16,6 @@
   val is_proof: state -> bool
   val is_skipped_proof: state -> bool
   val level: state -> int
-  val presentation_context_of: state -> Proof.context
   val previous_context_of: state -> Proof.context option
   val context_of: state -> Proof.context
   val generic_theory_of: state -> generic_theory
@@ -23,6 +23,8 @@
   val proof_of: state -> Proof.state
   val proof_position_of: state -> int
   val end_theory: Position.T -> state -> theory
+  val presentation_context: state -> Proof.context
+  val presentation_state: Proof.context -> state
   val pretty_context: state -> Pretty.T list
   val pretty_state: state -> Pretty.T list
   val string_of_state: state -> string
@@ -120,7 +122,8 @@
 
 datatype state = State of node option * node option;  (*current, previous*)
 
-fun theory_toplevel thy = State (SOME (Theory (Context.Theory thy, NONE)), NONE);
+fun generic_theory_toplevel gthy = State (SOME (Theory (gthy, NONE)), NONE);
+val theory_toplevel = generic_theory_toplevel o Context.Theory;
 
 val toplevel = State (NONE, NONE);
 
@@ -152,12 +155,6 @@
 
 fun node_case f g state = cases_node f g (node_of state);
 
-fun presentation_context_of state =
-  (case try node_of state of
-    SOME (Theory (_, SOME ctxt)) => ctxt
-  | SOME node => context_node node
-  | NONE => raise UNDEF);
-
 fun previous_context_of (State (_, NONE)) = NONE
   | previous_context_of (State (_, SOME prev)) = SOME (context_node prev);
 
@@ -176,6 +173,30 @@
   | end_theory pos (State (SOME _, _)) = error ("Unfinished theory" ^ Position.here pos);
 
 
+(* presentation context *)
+
+structure Presentation_State = Proof_Data
+(
+  type T = state option;
+  fun init _ = NONE;
+);
+
+fun presentation_context state =
+  (case try node_of state of
+    SOME (Theory (_, SOME ctxt)) => ctxt
+  | SOME node => context_node node
+  | NONE =>
+      (case try Theory.get_pure () of
+        SOME thy => Proof_Context.init_global thy
+      | NONE => raise UNDEF))
+  |> Presentation_State.put (SOME state);
+
+fun presentation_state ctxt =
+  (case Presentation_State.get ctxt of
+    NONE => generic_theory_toplevel (Context.Proof ctxt)
+  | SOME state => state);
+
+
 (* print state *)
 
 fun pretty_context state =
@@ -578,7 +599,7 @@
 fun transition int tr st =
   let
     val (st', opt_err) =
-      Context.setmp_generic_context (try (Context.Proof o presentation_context_of) st)
+      Context.setmp_generic_context (try (Context.Proof o presentation_context) st)
         (fn () => app int tr st) ();
     val opt_err' = opt_err |> Option.map
       (fn Runtime.EXCURSION_FAIL exn_info => exn_info
@@ -702,7 +723,7 @@
                       val (result, result_state) =
                         State (SOME (Proof (prf', (finish, orig_gthy))), prev)
                         |> fold_map (element_result keywords) body_elems ||> command end_tr;
-                    in (Result_List result, presentation_context_of result_state) end))
+                    in (Result_List result, presentation_context result_state) end))
               #> (fn (res, state') => state' |> put_result (Result_Future res));
 
             val forked_proof =
@@ -715,7 +736,7 @@
               |> command (head_tr |> reset_trans |> forked_proof);
             val end_result = Result (end_tr, st'');
             val result =
-              Result_List [head_result, Result.get (presentation_context_of st''), end_result];
+              Result_List [head_result, Result.get (presentation_context st''), end_result];
           in (result, st'') end
       end;
 
diff -r 2d9cf74943e1 -r aacea75450b4 src/Pure/ML/ml_file.ML
--- a/src/Pure/ML/ml_file.ML	Mon Jan 08 17:11:25 2018 +0000
+++ b/src/Pure/ML/ml_file.ML	Tue Jan 09 00:17:12 2018 +0100
@@ -18,6 +18,9 @@
     val [{src_path, lines, digest, pos}: Token.file] = files (Context.theory_of gthy);
     val provide = Resources.provide (src_path, digest);
     val source = Input.source true (cat_lines lines) (pos, pos);
+
+    val _ = Thy_Output.check_comments (Context.proof_of gthy) (Input.source_explode source);
+
     val flags =
       {SML = SML, exchange = false, redirect = true, verbose = true,
         debug = debug, writeln = writeln, warning = warning};
diff -r 2d9cf74943e1 -r aacea75450b4 src/Pure/ML/ml_pp.ML
--- a/src/Pure/ML/ml_pp.ML	Mon Jan 08 17:11:25 2018 +0000
+++ b/src/Pure/ML/ml_pp.ML	Tue Jan 09 00:17:12 2018 +0100
@@ -12,19 +12,19 @@
 
 val _ =
   ML_system_pp (fn depth => fn _ =>
-    ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_thm Thy_Info.pure_theory);
+    ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_thm Theory.get_pure);
 
 val _ =
   ML_system_pp (fn depth => fn _ =>
-    ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_cterm Thy_Info.pure_theory);
+    ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_cterm Theory.get_pure);
 
 val _ =
   ML_system_pp (fn depth => fn _ =>
-    ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_ctyp Thy_Info.pure_theory);
+    ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_ctyp Theory.get_pure);
 
 val _ =
   ML_system_pp (fn depth => fn _ =>
-    ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_typ Thy_Info.pure_theory);
+    ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_typ Theory.get_pure);
 
 
 local
diff -r 2d9cf74943e1 -r aacea75450b4 src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Mon Jan 08 17:11:25 2018 +0000
+++ b/src/Pure/PIDE/command.ML	Tue Jan 09 00:17:12 2018 +0100
@@ -195,14 +195,19 @@
       (fn () => Toplevel.command_exception int tr st); ([], SOME st))
   else Toplevel.command_errors int tr st;
 
-fun check_cmts span tr st' =
+fun check_error e =
+  (e (); []) handle exn =>
+    if Exn.is_interrupt exn then Exn.reraise exn
+    else Runtime.exn_messages exn;
+
+fun check_cmts ctxt span tr =
   Toplevel.setmp_thread_position tr
     (fn () =>
-      Outer_Syntax.side_comments span |> maps (fn cmt =>
-        (Thy_Output.output_text st' {markdown = false} (Token.input_of cmt); [])
-          handle exn =>
-            if Exn.is_interrupt exn then Exn.reraise exn
-            else Runtime.exn_messages exn)) ();
+      (span |> maps (fn tok =>
+        check_error (fn () => Thy_Output.check_token_comments ctxt tok))) @
+      (Outer_Syntax.side_comments span |> maps (fn tok =>
+        check_error (fn () => Thy_Output.output_text ctxt {markdown = false} (Token.input_of tok)))))
+    ();
 
 fun report tr m =
   Toplevel.setmp_thread_position tr (fn () => Output.report [Markup.markup_only m]) ();
@@ -234,7 +239,13 @@
     val _ = command_indent tr st;
     val _ = status tr Markup.running;
     val (errs1, result) = run keywords true tr st;
-    val errs2 = (case result of NONE => [] | SOME st' => check_cmts span tr st');
+    val errs2 =
+      (case result of
+        NONE => []
+      | SOME st' =>
+          (case try Toplevel.presentation_context st' of
+            NONE => []
+          | SOME ctxt' => check_cmts ctxt' span tr));
     val errs = errs1 @ errs2;
     val _ = List.app (Future.error_message (Toplevel.pos_of tr)) errs;
   in
diff -r 2d9cf74943e1 -r aacea75450b4 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Mon Jan 08 17:11:25 2018 +0000
+++ b/src/Pure/PIDE/document.ML	Tue Jan 09 00:17:12 2018 +0100
@@ -574,7 +574,7 @@
         |> Option.map (fn thy => (thy, (pos, Theory.get_markup thy))));
 
     val parents =
-      if null parents_reports then [Thy_Info.pure_theory ()] else map #1 parents_reports;
+      if null parents_reports then [Theory.get_pure ()] else map #1 parents_reports;
     val _ = Position.reports (map #2 parents_reports);
   in Resources.begin_theory master_dir header parents end;
 
diff -r 2d9cf74943e1 -r aacea75450b4 src/Pure/Thy/document_antiquotations.ML
--- a/src/Pure/Thy/document_antiquotations.ML	Mon Jan 08 17:11:25 2018 +0000
+++ b/src/Pure/Thy/document_antiquotations.ML	Tue Jan 09 00:17:12 2018 +0100
@@ -44,8 +44,8 @@
 
 fun control_antiquotation name s1 s2 =
   Thy_Output.antiquotation name (Scan.lift Args.cartouche_input)
-    (fn {state, ...} =>
-      enclose s1 s2 o Latex.output_text o Thy_Output.output_text state {markdown = false});
+    (fn {context = ctxt, ...} =>
+      enclose s1 s2 o Latex.output_text o Thy_Output.output_text ctxt {markdown = false});
 
 in
 
@@ -84,7 +84,7 @@
 val _ =
   Theory.setup
     (Thy_Output.antiquotation \<^binding>\<open>theory_text\<close> (Scan.lift Args.text_input)
-      (fn {state, context = ctxt, ...} => fn source =>
+      (fn {context = ctxt, ...} => fn source =>
         let
           val _ =
             Context_Position.report ctxt (Input.pos_of source)
@@ -101,7 +101,7 @@
           val indentation =
             Latex.output_symbols (replicate (Config.get ctxt Thy_Output.indent) Symbol.space);
         in
-          Latex.output_text (maps (Thy_Output.output_token state) toks) |>
+          Latex.output_text (maps (Thy_Output.output_token ctxt) toks) |>
            (if Config.get ctxt Thy_Output.display then
               split_lines #> map (prefix indentation) #> cat_lines #>
               Latex.environment "isabelle"
@@ -114,11 +114,11 @@
 local
 
 fun goal_state name main = Thy_Output.antiquotation name (Scan.succeed ())
-  (fn {state, context = ctxt, ...} => fn () =>
+  (fn {context = ctxt, ...} => fn () =>
     Thy_Output.output ctxt
       [Goal_Display.pretty_goal
         (Config.put Goal_Display.show_main_goal main ctxt)
-        (#goal (Proof.goal (Toplevel.proof_of state)))]);
+        (#goal (Proof.goal (Toplevel.proof_of (Toplevel.presentation_state ctxt))))]);
 
 in
 
diff -r 2d9cf74943e1 -r aacea75450b4 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Mon Jan 08 17:11:25 2018 +0000
+++ b/src/Pure/Thy/thy_info.ML	Tue Jan 09 00:17:12 2018 +0100
@@ -10,7 +10,6 @@
   val get_names: unit -> string list
   val lookup_theory: string -> theory option
   val get_theory: string -> theory
-  val pure_theory: unit -> theory
   val master_directory: string -> Path.T
   val remove_thy: string -> unit
   val use_theories:
@@ -102,8 +101,6 @@
     SOME theory => theory
   | _ => error ("Theory loader: undefined entry for theory " ^ quote name));
 
-fun pure_theory () = get_theory Context.PureN;
-
 val get_imports = Resources.imports_of o get_theory;
 
 
diff -r 2d9cf74943e1 -r aacea75450b4 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Mon Jan 08 17:11:25 2018 +0000
+++ b/src/Pure/Thy/thy_output.ML	Tue Jan 09 00:17:12 2018 +0100
@@ -19,13 +19,14 @@
   val check_option: Proof.context -> xstring * Position.T -> string
   val print_antiquotations: bool -> Proof.context -> unit
   val antiquotation: binding -> 'a context_parser ->
-    ({source: Token.src, state: Toplevel.state, context: Proof.context} -> 'a -> string) ->
-      theory -> theory
+    ({source: Token.src, context: Proof.context} -> 'a -> string) -> theory -> theory
   val boolean: string -> bool
   val integer: string -> int
-  val eval_antiquote: Toplevel.state -> Antiquote.text_antiquote -> string
-  val output_text: Toplevel.state -> {markdown: bool} -> Input.source -> Latex.text list
-  val output_token: Toplevel.state -> Token.T -> Latex.text list
+  val eval_antiquote: Proof.context -> Antiquote.text_antiquote -> string
+  val output_text: Proof.context -> {markdown: bool} -> Input.source -> Latex.text list
+  val check_comments: Proof.context -> Symbol_Pos.T list -> unit
+  val check_token_comments: Proof.context -> Token.T -> unit
+  val output_token: Proof.context -> Token.T -> Latex.text list
   val present_thy: theory -> (Toplevel.transition * Toplevel.state) list ->
     Token.T list -> Latex.text list
   val pretty_text: Proof.context -> string -> Pretty.T
@@ -37,8 +38,6 @@
   val string_of_margin: Proof.context -> Pretty.T -> string
   val output: Proof.context -> Pretty.T list -> string
   val verbatim_text: Proof.context -> string -> string
-  val document_command: {markdown: bool} ->
-    (xstring * Position.T) option * Input.source -> Toplevel.transition -> Toplevel.transition
 end;
 
 structure Thy_Output: THY_OUTPUT =
@@ -72,7 +71,7 @@
 structure Antiquotations = Theory_Data
 (
   type T =
-    (Token.src -> Toplevel.state -> Proof.context -> string) Name_Space.table *
+    (Token.src -> Proof.context -> string) Name_Space.table *
       (string -> Proof.context -> Proof.context) Name_Space.table;
   val empty : T =
     (Name_Space.empty_table Markup.document_antiquotationN,
@@ -95,9 +94,9 @@
 
 fun check_option ctxt = #1 o Name_Space.check (Context.Proof ctxt) (#2 (get_antiquotations ctxt));
 
-fun command src state ctxt =
+fun command src ctxt =
   let val (src', f) = Token.check_src ctxt (#1 o get_antiquotations) src
-  in f src' state ctxt end;
+  in f src' ctxt end;
 
 fun option ((xname, pos), s) ctxt =
   let
@@ -117,9 +116,9 @@
 
 fun antiquotation name scan body =
   add_command name
-    (fn src => fn state => fn ctxt =>
+    (fn src => fn ctxt =>
       let val (x, ctxt') = Token.syntax scan src ctxt
-      in body {source = src, state = state, context = ctxt'} x end);
+      in body {source = src, context = ctxt'} x end);
 
 
 
@@ -164,12 +163,12 @@
 
 local
 
-fun eval_antiq state (opts, src) =
+fun eval_antiq ctxt (opts, src) =
   let
-    val preview_ctxt = fold option opts (Toplevel.presentation_context_of state);
+    val preview_ctxt = fold option opts ctxt;
     val print_ctxt = Context_Position.set_visible false preview_ctxt;
 
-    fun cmd ctxt = wrap ctxt (fn () => command src state ctxt) ();
+    fun cmd ctxt = wrap ctxt (fn () => command src ctxt) ();
     val _ = cmd preview_ctxt;
     val print_modes = space_explode "," (Config.get print_ctxt modes) @ [Latex.latexN];
   in Print_Mode.with_modes print_modes (fn () => cmd print_ctxt) () end;
@@ -177,18 +176,12 @@
 in
 
 fun eval_antiquote _ (Antiquote.Text ss) = Symbol_Pos.content ss
-  | eval_antiquote state (Antiquote.Control {name, body, ...}) =
-      eval_antiq state
+  | eval_antiquote ctxt (Antiquote.Control {name, body, ...}) =
+      eval_antiq ctxt
         ([], Token.make_src name (if null body then [] else [Token.read_cartouche body]))
-  | eval_antiquote state (Antiquote.Antiq {range = (pos, _), body, ...}) =
-      let
-        val keywords =
-          (case try Toplevel.presentation_context_of state of
-            SOME ctxt => Thy_Header.get_keywords' ctxt
-          | NONE =>
-              error ("Unknown context -- cannot expand document antiquotations" ^
-                Position.here pos));
-      in eval_antiq state (Token.read_antiq keywords antiq (body, pos)) end;
+  | eval_antiquote ctxt (Antiquote.Antiq {range = (pos, _), body, ...}) =
+      let val keywords = Thy_Header.get_keywords' ctxt;
+      in eval_antiq ctxt (Token.read_antiq keywords antiq (body, pos)) end;
 
 end;
 
@@ -198,23 +191,15 @@
 
 (* output text *)
 
-fun output_text state {markdown} source =
+fun output_text ctxt {markdown} source =
   let
-    val is_reported =
-      (case try Toplevel.context_of state of
-        SOME ctxt => Context_Position.is_visible ctxt
-      | NONE => true);
-
     val pos = Input.pos_of source;
     val syms = Input.source_explode source;
 
-    val _ =
-      if is_reported then
-        Position.report pos (Markup.language_document (Input.is_delimited source))
-      else ();
+    val _ = Context_Position.report ctxt pos (Markup.language_document (Input.is_delimited source));
 
     val output_antiquotes =
-      map (fn ant => Latex.text (eval_antiquote state ant, #1 (Antiquote.range [ant])));
+      map (fn ant => Latex.text (eval_antiquote ctxt ant, #1 (Antiquote.range [ant])));
 
     fun output_line line =
       (if Markdown.line_is_item line then [Latex.string "\\item "] else []) @
@@ -226,20 +211,20 @@
           Latex.environment_block (Markdown.print_kind kind) (output_blocks body)
     and output_blocks blocks = separate (Latex.string "\n\n") (map output_block blocks);
   in
-    if Toplevel.is_skipped_proof state then []
+    if Toplevel.is_skipped_proof (Toplevel.presentation_state ctxt) then []
     else if markdown andalso exists (Markdown.is_control o Symbol_Pos.symbol) syms
     then
       let
         val ants = Antiquote.parse pos syms;
         val reports = Antiquote.antiq_reports ants;
         val blocks = Markdown.read_antiquotes ants;
-        val _ = if is_reported then Position.reports (reports @ Markdown.reports blocks) else ();
+        val _ = Context_Position.reports ctxt (reports @ Markdown.reports blocks);
       in output_blocks blocks end
     else
       let
         val ants = Antiquote.parse pos (Symbol_Pos.trim_blanks syms);
         val reports = Antiquote.antiq_reports ants;
-        val _ = if is_reported then Position.reports (reports @ Markdown.text_reports ants) else ();
+        val _ = Context_Position.reports ctxt (reports @ Markdown.text_reports ants);
       in output_antiquotes ants end
   end;
 
@@ -254,15 +239,15 @@
 val output_symbols_antiq =
   (fn Antiquote.Text syms => output_symbols syms
     | Antiquote.Control {name = (name, _), body, ...} =>
-        Latex.string ("\\isaantiqcontrol{" ^ Latex.output_symbols (Symbol.explode name) ^ "}") ::
+        Latex.string (Latex.output_symbols [Symbol.encode (Symbol.Control name)]) ::
           output_symbols body
     | Antiquote.Antiq {body, ...} =>
         Latex.enclose_body "%\n\\isaantiq\n" "{}%\n\\endisaantiq\n" (output_symbols body));
 
-fun output_symbols_comment state {antiq} (is_comment, syms) =
+fun output_symbols_comment ctxt {antiq} (is_comment, syms) =
   if is_comment then
     Latex.enclose_body ("%\n\\isamarkupcmt{") "}"
-      (output_text state {markdown = false}
+      (output_text ctxt {markdown = false}
         (Input.source true (Symbol_Pos.implode syms) (Symbol_Pos.range syms)))
   else if antiq then maps output_symbols_antiq (Antiquote.parse (#1 (Symbol_Pos.range syms)) syms)
   else output_symbols syms;
@@ -273,34 +258,43 @@
     Scan.option (Symbol_Pos.scan_cartouche_content "Document token error: ")
       >> (fn (syms, NONE) => (false, syms) | (_, SOME syms) => (true, syms));
 
+fun read_symbols_comment syms =
+  if exists (fn (s, _) => s = Symbol.comment) syms then
+    Scan.read Symbol_Pos.stopper (Scan.repeat scan_symbols_comment) syms
+  else NONE;
+
 in
 
-fun output_body state antiq bg en syms =
-  (if exists (fn (s, _) => s = Symbol.comment) syms then
-    (case Scan.read Symbol_Pos.stopper (Scan.repeat scan_symbols_comment) syms of
-      SOME res => maps (output_symbols_comment state {antiq = antiq}) res
-    | NONE => output_symbols syms)
-   else output_symbols syms) |> Latex.enclose_body bg en
-and output_token state tok =
+fun output_body ctxt antiq bg en syms =
+  (case read_symbols_comment syms of
+    SOME res => maps (output_symbols_comment ctxt {antiq = antiq}) res
+  | NONE => output_symbols syms) |> Latex.enclose_body bg en
+and output_token ctxt tok =
   let
-    val syms = Input.source_explode (Token.input_of tok);
-    val output =
-      if Token.is_kind Token.Comment tok then []
-      else if Token.is_command tok then output_body state false "\\isacommand{" "}" syms
-      else if Token.is_kind Token.Keyword tok andalso
-        Symbol.is_ascii_identifier (Token.content_of tok)
-      then output_body state false "\\isakeyword{" "}" syms
-      else if Token.is_kind Token.String tok then
-        output_body state false "{\\isachardoublequoteopen}" "{\\isachardoublequoteclose}" syms
-      else if Token.is_kind Token.Alt_String tok then
-        output_body state false "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}" syms
-      else if Token.is_kind Token.Verbatim tok then
-        output_body state true "{\\isacharverbatimopen}" "{\\isacharverbatimclose}" syms
-      else if Token.is_kind Token.Cartouche tok then
-        output_body state false "{\\isacartoucheopen}" "{\\isacartoucheclose}" syms
-      else output_body state false "" "" syms;
-  in output end
-  handle ERROR msg => error (msg ^ Position.here (Token.pos_of tok));
+    fun output antiq bg en =
+      output_body ctxt antiq bg en (Input.source_explode (Token.input_of tok));
+  in
+    (case Token.kind_of tok of
+      Token.Comment => []
+    | Token.Command => output false "\\isacommand{" "}"
+    | Token.Keyword =>
+        if Symbol.is_ascii_identifier (Token.content_of tok)
+        then output false "\\isakeyword{" "}"
+        else output false "" ""
+    | Token.String => output false "{\\isachardoublequoteopen}" "{\\isachardoublequoteclose}"
+    | Token.Alt_String => output false "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}"
+    | Token.Verbatim => output true "{\\isacharverbatimopen}" "{\\isacharverbatimclose}"
+    | Token.Cartouche => output false "{\\isacartoucheopen}" "{\\isacartoucheclose}"
+    | _ => output false "" "")
+  end handle ERROR msg => error (msg ^ Position.here (Token.pos_of tok));
+
+fun check_comments ctxt =
+  read_symbols_comment #> (Option.app o List.app) (fn (is_comment, syms) =>
+    (output_symbols_comment ctxt {antiq = false} (is_comment, syms);
+     if is_comment then check_comments ctxt syms else ()));
+
+fun check_token_comments ctxt tok =
+  check_comments ctxt (Input.source_explode (Token.input_of tok));
 
 end;
 
@@ -328,17 +322,17 @@
 val blank_token = basic_token Token.is_blank;
 val newline_token = basic_token Token.is_newline;
 
-fun present_token state tok =
+fun present_token ctxt tok =
   (case tok of
     Ignore_Token => []
-  | Basic_Token tok => output_token state tok
+  | Basic_Token tok => output_token ctxt tok
   | Markup_Token (cmd, source) =>
       Latex.enclose_body ("%\n\\isamarkup" ^ cmd ^ "{") "%\n}\n"
-        (output_text state {markdown = false} source)
+        (output_text ctxt {markdown = false} source)
   | Markup_Env_Token (cmd, source) =>
-      [Latex.environment_block ("isamarkup" ^ cmd) (output_text state {markdown = true} source)]
+      [Latex.environment_block ("isamarkup" ^ cmd) (output_text ctxt {markdown = true} source)]
   | Raw_Token source =>
-      Latex.string "%\n" :: output_text state {markdown = true} source @ [Latex.string "\n"]);
+      Latex.string "%\n" :: output_text ctxt {markdown = true} source @ [Latex.string "\n"]);
 
 
 (* command spans *)
@@ -381,11 +375,14 @@
 
 in
 
-fun present_span keywords document_tags span state state'
+fun present_span thy keywords document_tags span state state'
     (tag_stack, active_tag, newline, latex, present_cont) =
   let
+    val ctxt' =
+      Toplevel.presentation_context state'
+        handle Toplevel.UNDEF => Proof_Context.init_global (Context.get_theory thy Context.PureN);
     val present = fold (fn (tok, (flag, 0)) =>
-        fold cons (present_token state' tok)
+        fold cons (present_token ctxt' tok)
         #> cons (Latex.string flag)
       | _ => I);
 
@@ -558,7 +555,7 @@
 
     fun present_command tr span st st' =
       Toplevel.setmp_thread_position tr
-        (present_span keywords document_tags span st st');
+        (present_span thy keywords document_tags span st st');
 
     fun present _ [] = I
       | present st (((tr, st'), span) :: rest) = present_command tr span st st' #> present st' rest;
@@ -733,17 +730,4 @@
 
 end;
 
-
-
-(** document command **)
-
-fun document_command {markdown} (loc, txt) =
-  Toplevel.keep (fn state =>
-    (case loc of
-      NONE => ignore (output_text state {markdown = markdown} txt)
-    | SOME (_, pos) =>
-        error ("Illegal target specification -- not a theory context" ^ Position.here pos))) o
-  Toplevel.present_local_theory loc (fn state =>
-    ignore (output_text state {markdown = markdown} txt));
-
 end;
diff -r 2d9cf74943e1 -r aacea75450b4 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Mon Jan 08 17:11:25 2018 +0000
+++ b/src/Pure/Tools/build.scala	Tue Jan 09 00:17:12 2018 +0100
@@ -265,7 +265,8 @@
           val eval =
             "Command_Line.tool0 (fn () => (" +
             "Build.build " + ML_Syntax.print_string_bytes(File.standard_path(args_file)) +
-            (if (do_output) "; " + save_heap else "") + "));"
+            (if (Sessions.is_pure(name)) "; Theory.install_pure (Thy_Info.get_theory Context.PureN)"
+             else "") + (if (do_output) "; " + save_heap else "") + "));"
 
           val process =
             if (Sessions.is_pure(name)) {
diff -r 2d9cf74943e1 -r aacea75450b4 src/Pure/Tools/debugger.ML
--- a/src/Pure/Tools/debugger.ML	Mon Jan 08 17:11:25 2018 +0000
+++ b/src/Pure/Tools/debugger.ML	Tue Jan 09 00:17:12 2018 +0100
@@ -276,7 +276,7 @@
             if Command.eval_finished eval then
               let
                 val st = Command.eval_result_state eval;
-                val ctxt = Toplevel.presentation_context_of st
+                val ctxt = Toplevel.presentation_context st
                   handle Toplevel.UNDEF => err ();
               in
                 (case ML_Env.get_breakpoint (Context.Proof ctxt) breakpoint of
diff -r 2d9cf74943e1 -r aacea75450b4 src/Pure/Tools/rail.ML
--- a/src/Pure/Tools/rail.ML	Mon Jan 08 17:11:25 2018 +0000
+++ b/src/Pure/Tools/rail.ML	Tue Jan 09 00:17:12 2018 +0100
@@ -17,7 +17,7 @@
     Terminal of bool * string |
     Antiquote of bool * Antiquote.antiq
   val read: Proof.context -> Input.source -> (string Antiquote.antiquote * rail) list
-  val output_rules: Toplevel.state -> (string Antiquote.antiquote * rail) list -> string
+  val output_rules: Proof.context -> (string Antiquote.antiquote * rail) list -> string
 end;
 
 structure Rail: RAIL =
@@ -330,9 +330,9 @@
 
 in
 
-fun output_rules state rules =
+fun output_rules ctxt rules =
   let
-    val output_antiq = Thy_Output.eval_antiquote state o Antiquote.Antiq;
+    val output_antiq = Thy_Output.eval_antiquote ctxt o Antiquote.Antiq;
     fun output_text b s =
       Output.output s
       |> b ? enclose "\\isakeyword{" "}"
@@ -375,7 +375,7 @@
 
 val _ = Theory.setup
   (Thy_Output.antiquotation \<^binding>\<open>rail\<close> (Scan.lift Args.text_input)
-    (fn {state, context, ...} => output_rules state o read context));
+    (fn {context = ctxt, ...} => output_rules ctxt o read ctxt));
 
 end;
 
diff -r 2d9cf74943e1 -r aacea75450b4 src/Pure/pure_syn.ML
--- a/src/Pure/pure_syn.ML	Mon Jan 08 17:11:25 2018 +0000
+++ b/src/Pure/pure_syn.ML	Tue Jan 09 00:17:12 2018 +0100
@@ -7,6 +7,8 @@
 
 signature PURE_SYN =
 sig
+  val document_command: {markdown: bool} -> (xstring * Position.T) option * Input.source ->
+    Toplevel.transition -> Toplevel.transition
   val bootstrap_thy: theory
 end;
 
@@ -15,47 +17,52 @@
 
 val semi = Scan.option (Parse.$$$ ";");
 
+fun document_command {markdown} (loc, txt) =
+  Toplevel.keep (fn state =>
+    (case loc of
+      NONE =>
+        ignore (Thy_Output.output_text
+          (Toplevel.presentation_context state) {markdown = markdown} txt)
+    | SOME (_, pos) =>
+        error ("Illegal target specification -- not a theory context" ^ Position.here pos))) o
+  Toplevel.present_local_theory loc (fn state =>
+    ignore (Thy_Output.output_text (Toplevel.presentation_context state) {markdown = markdown} txt));
+
 val _ =
   Outer_Syntax.command ("chapter", \<^here>) "chapter heading"
-    (Parse.opt_target -- Parse.document_source --| semi
-      >> Thy_Output.document_command {markdown = false});
+    (Parse.opt_target -- Parse.document_source --| semi >> document_command {markdown = false});
 
 val _ =
   Outer_Syntax.command ("section", \<^here>) "section heading"
-    (Parse.opt_target -- Parse.document_source --| semi
-      >> Thy_Output.document_command {markdown = false});
+    (Parse.opt_target -- Parse.document_source --| semi >> document_command {markdown = false});
 
 val _ =
   Outer_Syntax.command ("subsection", \<^here>) "subsection heading"
-    (Parse.opt_target -- Parse.document_source --| semi
-      >> Thy_Output.document_command {markdown = false});
+    (Parse.opt_target -- Parse.document_source --| semi >> document_command {markdown = false});
 
 val _ =
   Outer_Syntax.command ("subsubsection", \<^here>) "subsubsection heading"
-    (Parse.opt_target -- Parse.document_source --| semi
-      >> Thy_Output.document_command {markdown = false});
+    (Parse.opt_target -- Parse.document_source --| semi >> document_command {markdown = false});
 
 val _ =
   Outer_Syntax.command ("paragraph", \<^here>) "paragraph heading"
-    (Parse.opt_target -- Parse.document_source --| semi
-      >> Thy_Output.document_command {markdown = false});
+    (Parse.opt_target -- Parse.document_source --| semi >> document_command {markdown = false});
 
 val _ =
   Outer_Syntax.command ("subparagraph", \<^here>) "subparagraph heading"
-    (Parse.opt_target -- Parse.document_source --| semi
-      >> Thy_Output.document_command {markdown = false});
+    (Parse.opt_target -- Parse.document_source --| semi >> document_command {markdown = false});
 
 val _ =
   Outer_Syntax.command ("text", \<^here>) "formal comment (primary style)"
-    (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = true});
+    (Parse.opt_target -- Parse.document_source >> document_command {markdown = true});
 
 val _ =
   Outer_Syntax.command ("txt", \<^here>) "formal comment (secondary style)"
-    (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = true});
+    (Parse.opt_target -- Parse.document_source >> document_command {markdown = true});
 
 val _ =
   Outer_Syntax.command ("text_raw", \<^here>) "LaTeX text (without surrounding environment)"
-    (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = true});
+    (Parse.opt_target -- Parse.document_source >> document_command {markdown = true});
 
 val _ =
   Outer_Syntax.command ("theory", \<^here>) "begin theory"
diff -r 2d9cf74943e1 -r aacea75450b4 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Mon Jan 08 17:11:25 2018 +0000
+++ b/src/Pure/theory.ML	Tue Jan 09 00:17:12 2018 +0100
@@ -11,6 +11,8 @@
   val nodes_of: theory -> theory list
   val setup: (theory -> theory) -> unit
   val local_setup: (Proof.context -> Proof.context) -> unit
+  val get_pure: unit -> theory
+  val install_pure: theory -> unit
   val get_markup: theory -> Markup.T
   val check: Proof.context -> string * Position.T -> theory
   val axiom_table: theory -> term Name_Space.table
@@ -45,6 +47,10 @@
 fun setup f = Context.>> (Context.map_theory f);
 fun local_setup f = Context.>> (Context.map_proof f);
 
+val pure: theory Single_Assignment.var = Single_Assignment.var "pure";
+fun get_pure () = the (Single_Assignment.peek pure);
+fun install_pure thy = Single_Assignment.assign pure thy;
+
 
 
 (** datatype thy **)