plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
authorwenzelm
Fri Nov 07 16:36:55 2014 +0100 (2014-11-07 ago)
changeset 5892823d0ffd48006
parent 58927 cf47382db395
child 58929 4aa9b3ab0b40
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
plain value Outer_Syntax within theory: parsing requires current theory context;
clarified name of Keyword.is_literal according to its semantics;
eliminated pointless type Keyword.T;
simplified @{command_spec};
clarified bootstrap keywords and syntax: take it as basis instead of side-branch;
NEWS
src/Doc/antiquote_setup.ML
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML
src/HOL/TPTP/sledgehammer_tactics.ML
src/HOL/Tools/ATP/atp_util.ML
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
src/HOL/Tools/Lifting/lifting_setup.ML
src/HOL/Tools/Nitpick/nitpick.ML
src/HOL/Tools/Nitpick/nitpick_scope.ML
src/HOL/Tools/Nitpick/nitpick_util.ML
src/HOL/Tools/Sledgehammer/sledgehammer.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML
src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
src/HOL/Tools/try0.ML
src/HOL/ex/Cartouche_Examples.thy
src/Pure/Isar/attrib.ML
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/keyword.ML
src/Pure/Isar/keyword.scala
src/Pure/Isar/outer_syntax.ML
src/Pure/ML/ml_antiquotations.ML
src/Pure/ML/ml_context.ML
src/Pure/ML/ml_file.ML
src/Pure/PIDE/command.ML
src/Pure/PIDE/document.ML
src/Pure/PIDE/protocol.ML
src/Pure/PIDE/resources.ML
src/Pure/PIDE/session.ML
src/Pure/PIDE/session.scala
src/Pure/Pure.thy
src/Pure/ROOT
src/Pure/ROOT.ML
src/Pure/Thy/thy_header.ML
src/Pure/Thy/thy_header.scala
src/Pure/Thy/thy_info.ML
src/Pure/Thy/thy_output.ML
src/Pure/Tools/build.ML
src/Pure/Tools/build.scala
src/Pure/Tools/find_consts.ML
src/Pure/Tools/find_theorems.ML
src/Pure/Tools/rail.ML
src/Pure/build-jars
src/Pure/pure_syn.ML
src/Pure/pure_syn.scala
src/Tools/Code/code_target.ML
src/Tools/jEdit/src/plugin.scala
     1.1 --- a/NEWS	Fri Nov 07 16:22:25 2014 +0100
     1.2 +++ b/NEWS	Fri Nov 07 16:36:55 2014 +0100
     1.3 @@ -18,6 +18,10 @@
     1.4  structure in the body: 'oops' is no longer supported here. Minor
     1.5  INCOMPATIBILITY, use 'sorry' instead.
     1.6  
     1.7 +* Outer syntax commands are managed authentically within the theory
     1.8 +context, without implicit global state.  Potential for accidental
     1.9 +INCOMPATIBILITY, make sure that required theories are really imported.
    1.10 +
    1.11  
    1.12  *** Prover IDE -- Isabelle/Scala/jEdit ***
    1.13  
     2.1 --- a/src/Doc/antiquote_setup.ML	Fri Nov 07 16:22:25 2014 +0100
     2.2 +++ b/src/Doc/antiquote_setup.ML	Fri Nov 07 16:36:55 2014 +0100
     2.3 @@ -191,16 +191,19 @@
     2.4  
     2.5  fun no_check _ _ = true;
     2.6  
     2.7 -fun is_keyword _ (name, _) =
     2.8 -  Keyword.is_keyword (Keyword.get_keywords ()) name;
     2.9 +fun is_keyword ctxt (name, _) =
    2.10 +  Keyword.is_literal (Thy_Header.get_keywords' ctxt) name;
    2.11  
    2.12  fun check_command ctxt (name, pos) =
    2.13 -  let val keywords = Keyword.get_keywords () in
    2.14 -    is_some (Keyword.command_keyword keywords name) andalso
    2.15 +  let
    2.16 +    val thy = Proof_Context.theory_of ctxt;
    2.17 +    val keywords = Thy_Header.get_keywords thy;
    2.18 +  in
    2.19 +    Keyword.is_command keywords name andalso
    2.20        let
    2.21          val markup =
    2.22            Outer_Syntax.scan keywords Position.none name
    2.23 -          |> maps (Outer_Syntax.command_reports (#2 (Outer_Syntax.get_syntax ())))
    2.24 +          |> maps (Outer_Syntax.command_reports thy)
    2.25            |> map (snd o fst);
    2.26          val _ = Context_Position.reports ctxt (map (pair pos) markup);
    2.27        in true end
     3.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Nov 07 16:22:25 2014 +0100
     3.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Nov 07 16:36:55 2014 +0100
     3.3 @@ -414,7 +414,7 @@
     3.4           time_isa) = time_limit (Mirabelle.cpu_time (fn () =>
     3.5        let
     3.6          val ho_atp = Sledgehammer_Prover_ATP.is_ho_atp ctxt prover_name
     3.7 -        val keywords = Keyword.get_keywords ()
     3.8 +        val keywords = Thy_Header.get_keywords' ctxt
     3.9          val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
    3.10          val facts =
    3.11            Sledgehammer_Fact.nearly_all_facts ctxt ho_atp
    3.12 @@ -535,8 +535,8 @@
    3.13      fun do_method named_thms ctxt =
    3.14        let
    3.15          val ref_of_str =
    3.16 -          suffix ";" #> Outer_Syntax.scan (Keyword.get_keywords ()) Position.none #> Parse.xthm
    3.17 -          #> fst
    3.18 +          suffix ";" #> Outer_Syntax.scan (Thy_Header.get_keywords' ctxt) Position.none
    3.19 +          #> Parse.xthm #> fst
    3.20          val thms = named_thms |> maps snd
    3.21          val facts = named_thms |> map (ref_of_str o fst o fst)
    3.22          val fact_override = {add = facts, del = [], only = true}
    3.23 @@ -561,7 +561,7 @@
    3.24            let
    3.25              val (type_encs, lam_trans) =
    3.26                !meth
    3.27 -              |> Outer_Syntax.scan (Keyword.get_keywords ()) Position.start
    3.28 +              |> Outer_Syntax.scan (Thy_Header.get_keywords' ctxt) Position.start
    3.29                |> filter Token.is_proper |> tl
    3.30                |> Metis_Tactic.parse_metis_options |> fst
    3.31                |>> the_default [ATP_Proof_Reconstruct.partial_typesN]
     4.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Fri Nov 07 16:22:25 2014 +0100
     4.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Fri Nov 07 16:36:55 2014 +0100
     4.3 @@ -110,7 +110,7 @@
     4.4           val subgoal = 1
     4.5           val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal subgoal ctxt
     4.6           val ho_atp = Sledgehammer_Prover_ATP.is_ho_atp ctxt prover
     4.7 -         val keywords = Keyword.get_keywords ()
     4.8 +         val keywords = Thy_Header.get_keywords' ctxt
     4.9           val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
    4.10           val facts =
    4.11             Sledgehammer_Fact.nearly_all_facts ctxt ho_atp
     5.1 --- a/src/HOL/TPTP/sledgehammer_tactics.ML	Fri Nov 07 16:22:25 2014 +0100
     5.2 +++ b/src/HOL/TPTP/sledgehammer_tactics.ML	Fri Nov 07 16:36:55 2014 +0100
     5.3 @@ -36,7 +36,7 @@
     5.4      val default_max_facts = default_max_facts_of_prover ctxt name
     5.5      val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal i ctxt
     5.6      val ho_atp = exists (is_ho_atp ctxt) provers
     5.7 -    val keywords = Keyword.get_keywords ()
     5.8 +    val keywords = Thy_Header.get_keywords' ctxt
     5.9      val css_table = clasimpset_rule_table_of ctxt
    5.10      val facts =
    5.11        nearly_all_facts ctxt ho_atp fact_override keywords css_table chained hyp_ts concl_t
     6.1 --- a/src/HOL/Tools/ATP/atp_util.ML	Fri Nov 07 16:22:25 2014 +0100
     6.2 +++ b/src/HOL/Tools/ATP/atp_util.ML	Fri Nov 07 16:36:55 2014 +0100
     6.3 @@ -19,7 +19,7 @@
     6.4    val nat_subscript : int -> string
     6.5    val unquote_tvar : string -> string
     6.6    val unyxml : string -> string
     6.7 -  val maybe_quote : string -> string
     6.8 +  val maybe_quote : Keyword.keywords -> string -> string
     6.9    val string_of_ext_time : bool * Time.time -> string
    6.10    val string_of_time : Time.time -> string
    6.11    val type_instance : theory -> typ -> typ -> bool
    6.12 @@ -136,11 +136,11 @@
    6.13  val unyxml = XML.content_of o YXML.parse_body
    6.14  
    6.15  val is_long_identifier = forall Symbol_Pos.is_identifier o Long_Name.explode
    6.16 -fun maybe_quote y =
    6.17 +fun maybe_quote keywords y =
    6.18    let val s = unyxml y in
    6.19      y |> ((not (is_long_identifier (unquote_tvar s)) andalso
    6.20             not (is_long_identifier (unquery_var s))) orelse
    6.21 -           Keyword.is_keyword (Keyword.get_keywords ()) s) ? quote
    6.22 +           Keyword.is_literal keywords s) ? quote
    6.23    end
    6.24  
    6.25  fun string_of_ext_time (plus, time) =
     7.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Fri Nov 07 16:22:25 2014 +0100
     7.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Fri Nov 07 16:36:55 2014 +0100
     7.3 @@ -2016,7 +2016,7 @@
     7.4              val fake_T = qsoty (unfreeze_fp X);
     7.5              val fake_T_backdrop = qsoty (unfreeze_fp X_backdrop);
     7.6              fun register_hint () =
     7.7 -              "\nUse the " ^ quote (fst (fst @{command_spec "bnf"})) ^ " command to register " ^
     7.8 +              "\nUse the " ^ quote (#1 @{command_spec "bnf"}) ^ " command to register " ^
     7.9                quote bad_tc ^ " as a bounded natural functor to allow nested (co)recursion through \
    7.10                \it";
    7.11            in
     8.1 --- a/src/HOL/Tools/Lifting/lifting_setup.ML	Fri Nov 07 16:22:25 2014 +0100
     8.2 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Fri Nov 07 16:36:55 2014 +0100
     8.3 @@ -221,7 +221,7 @@
     8.4  
     8.5      val thy = Proof_Context.theory_of lthy
     8.6      val dummy_thm = Thm.transfer thy Drule.dummy_thm
     8.7 -    val pointer = Outer_Syntax.scan (Keyword.get_keywords ()) Position.none bundle_name
     8.8 +    val pointer = Outer_Syntax.scan (Thy_Header.get_keywords thy) Position.none bundle_name
     8.9      val restore_lifting_att = 
    8.10        ([dummy_thm], [Token.src ("Lifting.lifting_restore_internal", Position.none) pointer])
    8.11    in
     9.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Fri Nov 07 16:22:25 2014 +0100
     9.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Fri Nov 07 16:36:55 2014 +0100
     9.3 @@ -220,6 +220,7 @@
     9.4      val timer = Timer.startRealTimer ()
     9.5      val thy = Proof.theory_of state
     9.6      val ctxt = Proof.context_of state
     9.7 +    val keywords = Thy_Header.get_keywords thy
     9.8  (* FIXME: reintroduce code before new release:
     9.9  
    9.10      val nitpick_thy = Thy_Info.get_theory "Nitpick"
    9.11 @@ -365,7 +366,7 @@
    9.12  
    9.13      val unique_scope = forall (curry (op =) 1 o length o snd) cards_assigns
    9.14      fun monotonicity_message Ts extra =
    9.15 -      let val pretties = map (pretty_maybe_quote o pretty_for_type ctxt) Ts in
    9.16 +      let val pretties = map (pretty_maybe_quote keywords o pretty_for_type ctxt) Ts in
    9.17          Pretty.blk (0,
    9.18            pstrs ("The type" ^ plural_s_for_list pretties ^ " ") @
    9.19            pretty_serial_commas "and" pretties @
    10.1 --- a/src/HOL/Tools/Nitpick/nitpick_scope.ML	Fri Nov 07 16:22:25 2014 +0100
    10.2 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML	Fri Nov 07 16:36:55 2014 +0100
    10.3 @@ -180,9 +180,10 @@
    10.4    let
    10.5      fun standard_blocks s = map (Pretty.block o cons (Pretty.str (s ^ " ")))
    10.6      val (primary_cards, secondary_cards, maxes, iters, miscs) =
    10.7 -      quintuple_for_scope (pretty_maybe_quote oo pretty_for_type)
    10.8 -                          (pretty_maybe_quote oo Syntax.pretty_term)
    10.9 -                          Pretty.str scope
   10.10 +      quintuple_for_scope
   10.11 +        (fn ctxt => pretty_maybe_quote (Thy_Header.get_keywords' ctxt) o pretty_for_type ctxt)
   10.12 +        (fn ctxt => pretty_maybe_quote (Thy_Header.get_keywords' ctxt) o Syntax.pretty_term ctxt)
   10.13 +        Pretty.str scope
   10.14    in
   10.15      standard_blocks "card" primary_cards @
   10.16      (if verbose then
    11.1 --- a/src/HOL/Tools/Nitpick/nitpick_util.ML	Fri Nov 07 16:22:25 2014 +0100
    11.2 +++ b/src/HOL/Tools/Nitpick/nitpick_util.ML	Fri Nov 07 16:36:55 2014 +0100
    11.3 @@ -72,7 +72,7 @@
    11.4    val indent_size : int
    11.5    val pstrs : string -> Pretty.T list
    11.6    val unyxml : string -> string
    11.7 -  val pretty_maybe_quote : Pretty.T -> Pretty.T
    11.8 +  val pretty_maybe_quote : Keyword.keywords -> Pretty.T -> Pretty.T
    11.9    val hash_term : term -> int
   11.10    val spying : bool -> (unit -> Proof.state * int * string) -> unit
   11.11  end;
   11.12 @@ -287,9 +287,9 @@
   11.13  
   11.14  val maybe_quote = ATP_Util.maybe_quote
   11.15  
   11.16 -fun pretty_maybe_quote pretty =
   11.17 +fun pretty_maybe_quote keywords pretty =
   11.18    let val s = Pretty.str_of pretty in
   11.19 -    if maybe_quote s = s then pretty else Pretty.enum "" "\"" "\"" [pretty]
   11.20 +    if maybe_quote keywords s = s then pretty else Pretty.enum "" "\"" "\"" [pretty]
   11.21    end
   11.22  
   11.23  val hashw = ATP_Util.hashw
    12.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Fri Nov 07 16:22:25 2014 +0100
    12.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Fri Nov 07 16:36:55 2014 +0100
    12.3 @@ -264,10 +264,10 @@
    12.4          val print =
    12.5            if mode = Normal andalso is_none output_result then writeln else K ()
    12.6          val ctxt = Proof.context_of state
    12.7 +        val keywords = Thy_Header.get_keywords' ctxt
    12.8          val {facts = chained, goal, ...} = Proof.goal state
    12.9          val (_, hyp_ts, concl_t) = strip_subgoal goal i ctxt
   12.10          val ho_atp = exists (is_ho_atp ctxt) provers
   12.11 -        val keywords = Keyword.get_keywords ()
   12.12          val css = clasimpset_rule_table_of ctxt
   12.13          val all_facts =
   12.14            nearly_all_facts ctxt ho_atp fact_override keywords css chained hyp_ts concl_t
    13.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Fri Nov 07 16:22:25 2014 +0100
    13.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Fri Nov 07 16:36:55 2014 +0100
    13.3 @@ -67,7 +67,7 @@
    13.4  val no_fact_override = {add = [], del = [], only = false}
    13.5  
    13.6  fun needs_quoting keywords s =
    13.7 -  Keyword.is_keyword keywords s orelse
    13.8 +  Keyword.is_literal keywords s orelse
    13.9    exists (not o Symbol_Pos.is_identifier) (Long_Name.explode s)
   13.10  
   13.11  fun make_name keywords multi j name =
    14.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Fri Nov 07 16:22:25 2014 +0100
    14.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Fri Nov 07 16:36:55 2014 +0100
    14.3 @@ -267,6 +267,8 @@
    14.4  
    14.5  fun string_of_isar_proof ctxt0 i n proof =
    14.6    let
    14.7 +    val keywords = Thy_Header.get_keywords' ctxt0
    14.8 +
    14.9      (* Make sure only type constraints inserted by the type annotation code are printed. *)
   14.10      val ctxt = ctxt0
   14.11        |> Config.put show_markup false
   14.12 @@ -300,7 +302,7 @@
   14.13              |> annotate_types_in_term ctxt
   14.14              |> with_vanilla_print_mode (Syntax.unparse_term ctxt #> Pretty.string_of)
   14.15              |> simplify_spaces
   14.16 -            |> maybe_quote),
   14.17 +            |> maybe_quote keywords),
   14.18         ctxt |> perhaps (try (Variable.auto_fixes term)))
   14.19  
   14.20      fun using_facts [] [] = ""
   14.21 @@ -317,8 +319,8 @@
   14.22        end
   14.23  
   14.24      fun of_free (s, T) =
   14.25 -      maybe_quote s ^ " :: " ^
   14.26 -      maybe_quote (simplify_spaces (with_vanilla_print_mode (Syntax.string_of_typ ctxt) T))
   14.27 +      maybe_quote keywords s ^ " :: " ^
   14.28 +      maybe_quote keywords (simplify_spaces (with_vanilla_print_mode (Syntax.string_of_typ ctxt) T))
   14.29  
   14.30      fun add_frees xs (s, ctxt) =
   14.31        (s ^ space_implode " and " (map of_free xs), ctxt |> fold Variable.auto_fixes (map Free xs))
    15.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Nov 07 16:22:25 2014 +0100
    15.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Nov 07 16:36:55 2014 +0100
    15.3 @@ -123,7 +123,7 @@
    15.4  fun thms_of_name ctxt name =
    15.5    let
    15.6      val get = maps (Proof_Context.get_fact ctxt o fst)
    15.7 -    val keywords = Keyword.get_keywords ()
    15.8 +    val keywords = Thy_Header.get_keywords' ctxt
    15.9    in
   15.10      Source.of_string name
   15.11      |> Symbol.source
    16.1 --- a/src/HOL/Tools/try0.ML	Fri Nov 07 16:22:25 2014 +0100
    16.2 +++ b/src/HOL/Tools/try0.ML	Fri Nov 07 16:36:55 2014 +0100
    16.3 @@ -41,15 +41,15 @@
    16.4        NONE
    16.5    end;
    16.6  
    16.7 -fun parse_method s =
    16.8 +fun parse_method keywords s =
    16.9    enclose "(" ")" s
   16.10 -  |> Outer_Syntax.scan (Keyword.get_keywords ()) Position.start
   16.11 +  |> Outer_Syntax.scan keywords Position.start
   16.12    |> filter Token.is_proper
   16.13    |> Scan.read Token.stopper Method.parse
   16.14    |> (fn SOME (Method.Source src, _) => src | _ => raise Fail "expected Source");
   16.15  
   16.16  fun apply_named_method_on_first_goal ctxt =
   16.17 -  parse_method
   16.18 +  parse_method (Thy_Header.get_keywords' ctxt)
   16.19    #> Method.method_cmd ctxt
   16.20    #> Method.Basic
   16.21    #> (fn m => Method.Combinator (Method.no_combinator_info, Method.Select_Goals 1, [m]))
    17.1 --- a/src/HOL/ex/Cartouche_Examples.thy	Fri Nov 07 16:22:25 2014 +0100
    17.2 +++ b/src/HOL/ex/Cartouche_Examples.thy	Fri Nov 07 16:36:55 2014 +0100
    17.3 @@ -178,7 +178,7 @@
    17.4  ML {*
    17.5    Outer_Syntax.command
    17.6      @{command_spec "text_cartouche"} ""
    17.7 -    (Parse.opt_target -- Parse.source_position Parse.cartouche >> Isar_Cmd.local_theory_markup)
    17.8 +    (Parse.opt_target -- Parse.source_position Parse.cartouche >> Thy_Output.local_theory_markup)
    17.9  *}
   17.10  
   17.11  text_cartouche
    18.1 --- a/src/Pure/Isar/attrib.ML	Fri Nov 07 16:22:25 2014 +0100
    18.2 +++ b/src/Pure/Isar/attrib.ML	Fri Nov 07 16:36:55 2014 +0100
    18.3 @@ -288,8 +288,8 @@
    18.4  
    18.5  fun read_attribs ctxt source =
    18.6    let
    18.7 +    val keywords = Thy_Header.get_keywords' ctxt;
    18.8      val syms = Symbol_Pos.source_explode source;
    18.9 -    val keywords = Keyword.get_keywords ();
   18.10    in
   18.11      (case Token.read_no_commands keywords Parse.attribs syms of
   18.12        [raw_srcs] => check_attribs ctxt raw_srcs
    19.1 --- a/src/Pure/Isar/isar_cmd.ML	Fri Nov 07 16:22:25 2014 +0100
    19.2 +++ b/src/Pure/Isar/isar_cmd.ML	Fri Nov 07 16:36:55 2014 +0100
    19.3 @@ -48,12 +48,6 @@
    19.4    val print_term: (string list * string) -> Toplevel.transition -> Toplevel.transition
    19.5    val print_type: (string list * (string * string option)) ->
    19.6      Toplevel.transition -> Toplevel.transition
    19.7 -  val local_theory_markup: (xstring * Position.T) option * Symbol_Pos.source ->
    19.8 -    Toplevel.transition -> Toplevel.transition
    19.9 -  val proof_markup: Symbol_Pos.source -> Toplevel.transition -> Toplevel.transition
   19.10 -  val header_markup: Symbol_Pos.source -> Toplevel.transition -> Toplevel.transition
   19.11 -  val heading_markup: (xstring * Position.T) option * Symbol_Pos.source ->
   19.12 -    Toplevel.transition -> Toplevel.transition
   19.13  end;
   19.14  
   19.15  structure Isar_Cmd: ISAR_CMD =
   19.16 @@ -376,28 +370,4 @@
   19.17  
   19.18  end;
   19.19  
   19.20 -
   19.21 -(* markup commands *)
   19.22 -
   19.23 -fun local_theory_markup (loc, txt) = Toplevel.present_local_theory loc (Thy_Output.check_text txt);
   19.24 -val proof_markup = Toplevel.present_proof o Thy_Output.check_text;
   19.25 -
   19.26 -fun reject_target NONE = ()
   19.27 -  | reject_target (SOME (_, pos)) =
   19.28 -      error ("Illegal target specification -- not a theory context" ^ Position.here pos);
   19.29 -
   19.30 -fun header_markup txt =
   19.31 -  Toplevel.keep (fn state =>
   19.32 -    if Toplevel.is_toplevel state then
   19.33 -     (legacy_feature "Obsolete 'header' command -- use 'chapter', 'section' etc. instead";
   19.34 -      Thy_Output.check_text txt state)
   19.35 -    else raise Toplevel.UNDEF);
   19.36 -
   19.37 -fun heading_markup (loc, txt) =
   19.38 -  Toplevel.keep (fn state =>
   19.39 -    if Toplevel.is_toplevel state then (reject_target loc; Thy_Output.check_text txt state)
   19.40 -    else raise Toplevel.UNDEF) o
   19.41 -  local_theory_markup (loc, txt) o
   19.42 -  Toplevel.present_proof (fn state => (reject_target loc; Thy_Output.check_text txt state));
   19.43 -
   19.44  end;
    20.1 --- a/src/Pure/Isar/isar_syn.ML	Fri Nov 07 16:22:25 2014 +0100
    20.2 +++ b/src/Pure/Isar/isar_syn.ML	Fri Nov 07 16:36:55 2014 +0100
    20.3 @@ -10,49 +10,24 @@
    20.4  (** markup commands **)
    20.5  
    20.6  val _ =
    20.7 -  Outer_Syntax.markup_command Thy_Output.Markup
    20.8 -    @{command_spec "header"} "theory header"
    20.9 -    (Parse.document_source >> Isar_Cmd.header_markup);
   20.10 -
   20.11 -val _ =
   20.12 -  Outer_Syntax.markup_command Thy_Output.Markup
   20.13 -    @{command_spec "chapter"} "chapter heading"
   20.14 -    (Parse.opt_target -- Parse.document_source >> Isar_Cmd.heading_markup);
   20.15 -
   20.16 -val _ =
   20.17 -  Outer_Syntax.markup_command Thy_Output.Markup
   20.18 -    @{command_spec "section"} "section heading"
   20.19 -    (Parse.opt_target -- Parse.document_source >> Isar_Cmd.heading_markup);
   20.20 -
   20.21 -val _ =
   20.22 -  Outer_Syntax.markup_command Thy_Output.Markup
   20.23 -    @{command_spec "subsection"} "subsection heading"
   20.24 -    (Parse.opt_target -- Parse.document_source >> Isar_Cmd.heading_markup);
   20.25 +  Outer_Syntax.markup_command Outer_Syntax.Markup_Env
   20.26 +    @{command_spec "text"} "formal comment (theory)"
   20.27 +    (Parse.opt_target -- Parse.document_source >> Thy_Output.local_theory_markup);
   20.28  
   20.29  val _ =
   20.30 -  Outer_Syntax.markup_command Thy_Output.Markup
   20.31 -    @{command_spec "subsubsection"} "subsubsection heading"
   20.32 -    (Parse.opt_target -- Parse.document_source >> Isar_Cmd.heading_markup);
   20.33 -
   20.34 -val _ =
   20.35 -  Outer_Syntax.markup_command Thy_Output.MarkupEnv
   20.36 -    @{command_spec "text"} "formal comment (theory)"
   20.37 -    (Parse.opt_target -- Parse.document_source >> Isar_Cmd.local_theory_markup);
   20.38 +  Outer_Syntax.markup_command Outer_Syntax.Verbatim
   20.39 +    @{command_spec "text_raw"} "raw document preparation text"
   20.40 +    (Parse.opt_target -- Parse.document_source >> Thy_Output.local_theory_markup);
   20.41  
   20.42  val _ =
   20.43 -  Outer_Syntax.markup_command Thy_Output.Verbatim
   20.44 -    @{command_spec "text_raw"} "raw document preparation text"
   20.45 -    (Parse.opt_target -- Parse.document_source >> Isar_Cmd.local_theory_markup);
   20.46 +  Outer_Syntax.markup_command Outer_Syntax.Markup_Env
   20.47 +    @{command_spec "txt"} "formal comment (proof)"
   20.48 +    (Parse.document_source >> Thy_Output.proof_markup);
   20.49  
   20.50  val _ =
   20.51 -  Outer_Syntax.markup_command Thy_Output.MarkupEnv
   20.52 -    @{command_spec "txt"} "formal comment (proof)"
   20.53 -    (Parse.document_source >> Isar_Cmd.proof_markup);
   20.54 -
   20.55 -val _ =
   20.56 -  Outer_Syntax.markup_command Thy_Output.Verbatim
   20.57 +  Outer_Syntax.markup_command Outer_Syntax.Verbatim
   20.58      @{command_spec "txt_raw"} "raw document preparation text (proof)"
   20.59 -    (Parse.document_source >> Isar_Cmd.proof_markup);
   20.60 +    (Parse.document_source >> Thy_Output.proof_markup);
   20.61  
   20.62  
   20.63  
   20.64 @@ -730,11 +705,11 @@
   20.65    Outer_Syntax.command @{command_spec "help"}
   20.66      "retrieve outer syntax commands according to name patterns"
   20.67      (Scan.repeat Parse.name >>
   20.68 -      (fn pats => Toplevel.imperative (fn () => Outer_Syntax.help_syntax pats)));
   20.69 +      (fn pats => Toplevel.keep (fn st => Outer_Syntax.help_syntax (Toplevel.theory_of st) pats)));
   20.70  
   20.71  val _ =
   20.72    Outer_Syntax.command @{command_spec "print_commands"} "print outer syntax commands"
   20.73 -    (Scan.succeed (Toplevel.imperative Outer_Syntax.print_syntax));
   20.74 +    (Scan.succeed (Toplevel.keep (Outer_Syntax.print_syntax o Toplevel.theory_of)));
   20.75  
   20.76  val _ =
   20.77    Outer_Syntax.command @{command_spec "print_options"} "print configuration options"
    21.1 --- a/src/Pure/Isar/keyword.ML	Fri Nov 07 16:22:25 2014 +0100
    21.2 +++ b/src/Pure/Isar/keyword.ML	Fri Nov 07 16:36:55 2014 +0100
    21.3 @@ -6,43 +6,38 @@
    21.4  
    21.5  signature KEYWORD =
    21.6  sig
    21.7 -  type T
    21.8 -  val kind_of: T -> string
    21.9 -  val kind_files_of: T -> string * string list
   21.10 -  val diag: T
   21.11 -  val heading: T
   21.12 -  val thy_begin: T
   21.13 -  val thy_end: T
   21.14 -  val thy_decl: T
   21.15 -  val thy_decl_block: T
   21.16 -  val thy_load: T
   21.17 -  val thy_goal: T
   21.18 -  val qed: T
   21.19 -  val qed_script: T
   21.20 -  val qed_block: T
   21.21 -  val qed_global: T
   21.22 -  val prf_goal: T
   21.23 -  val prf_block: T
   21.24 -  val prf_open: T
   21.25 -  val prf_close: T
   21.26 -  val prf_chain: T
   21.27 -  val prf_decl: T
   21.28 -  val prf_asm: T
   21.29 -  val prf_asm_goal: T
   21.30 -  val prf_asm_goal_script: T
   21.31 -  val prf_script: T
   21.32 +  val diag: string
   21.33 +  val heading: string
   21.34 +  val thy_begin: string
   21.35 +  val thy_end: string
   21.36 +  val thy_decl: string
   21.37 +  val thy_decl_block: string
   21.38 +  val thy_load: string
   21.39 +  val thy_goal: string
   21.40 +  val qed: string
   21.41 +  val qed_script: string
   21.42 +  val qed_block: string
   21.43 +  val qed_global: string
   21.44 +  val prf_goal: string
   21.45 +  val prf_block: string
   21.46 +  val prf_open: string
   21.47 +  val prf_close: string
   21.48 +  val prf_chain: string
   21.49 +  val prf_decl: string
   21.50 +  val prf_asm: string
   21.51 +  val prf_asm_goal: string
   21.52 +  val prf_asm_goal_script: string
   21.53 +  val prf_script: string
   21.54    type spec = (string * string list) * string list
   21.55 -  val check_spec: spec -> T
   21.56 -  val command_spec: (string * spec) * Position.T -> (string * T) * Position.T
   21.57    type keywords
   21.58    val minor_keywords: keywords -> Scan.lexicon
   21.59    val major_keywords: keywords -> Scan.lexicon
   21.60    val no_command_keywords: keywords -> keywords
   21.61    val empty_keywords: keywords
   21.62    val merge_keywords: keywords * keywords -> keywords
   21.63 -  val add_keywords: string * T option -> keywords -> keywords
   21.64 -  val is_keyword: keywords -> string -> bool
   21.65 -  val command_keyword: keywords -> string -> T option
   21.66 +  val add_keywords: (string * spec option) list -> keywords -> keywords
   21.67 +  val is_literal: keywords -> string -> bool
   21.68 +  val is_command: keywords -> string -> bool
   21.69    val command_files: keywords -> string -> Path.T -> Path.T list
   21.70    val command_tags: keywords -> string -> string list
   21.71    val is_diag: keywords -> string -> bool
   21.72 @@ -58,8 +53,6 @@
   21.73    val is_qed: keywords -> string -> bool
   21.74    val is_qed_global: keywords -> string -> bool
   21.75    val is_printed: keywords -> string -> bool
   21.76 -  val define: string * T option -> unit
   21.77 -  val get_keywords: unit -> keywords
   21.78  end;
   21.79  
   21.80  structure Keyword: KEYWORD =
   21.81 @@ -69,57 +62,50 @@
   21.82  
   21.83  (* kinds *)
   21.84  
   21.85 -datatype T = Keyword of
   21.86 +val diag = "diag";
   21.87 +val heading = "heading";
   21.88 +val thy_begin = "thy_begin";
   21.89 +val thy_end = "thy_end";
   21.90 +val thy_decl = "thy_decl";
   21.91 +val thy_decl_block = "thy_decl_block";
   21.92 +val thy_load = "thy_load";
   21.93 +val thy_goal = "thy_goal";
   21.94 +val qed = "qed";
   21.95 +val qed_script = "qed_script";
   21.96 +val qed_block = "qed_block";
   21.97 +val qed_global = "qed_global";
   21.98 +val prf_goal = "prf_goal";
   21.99 +val prf_block = "prf_block";
  21.100 +val prf_open = "prf_open";
  21.101 +val prf_close = "prf_close";
  21.102 +val prf_chain = "prf_chain";
  21.103 +val prf_decl = "prf_decl";
  21.104 +val prf_asm = "prf_asm";
  21.105 +val prf_asm_goal = "prf_asm_goal";
  21.106 +val prf_asm_goal_script = "prf_asm_goal_script";
  21.107 +val prf_script = "prf_script";
  21.108 +
  21.109 +val kinds =
  21.110 +  [diag, heading, thy_begin, thy_end, thy_load, thy_decl, thy_decl_block, thy_goal,
  21.111 +    qed, qed_script, qed_block, qed_global, prf_goal, prf_block, prf_open, prf_close,
  21.112 +    prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_asm_goal_script, prf_script];
  21.113 +
  21.114 +
  21.115 +(* specifications *)
  21.116 +
  21.117 +type T =
  21.118   {kind: string,
  21.119    files: string list,  (*extensions of embedded files*)
  21.120    tags: string list};
  21.121  
  21.122 -fun kind s = Keyword {kind = s, files = [], tags = []};
  21.123 -fun kind_of (Keyword {kind, ...}) = kind;
  21.124 -fun kind_files_of (Keyword {kind, files, ...}) = (kind, files);
  21.125 -
  21.126 -val diag = kind "diag";
  21.127 -val heading = kind "heading";
  21.128 -val thy_begin = kind "thy_begin";
  21.129 -val thy_end = kind "thy_end";
  21.130 -val thy_decl = kind "thy_decl";
  21.131 -val thy_decl_block = kind "thy_decl_block";
  21.132 -val thy_load = kind "thy_load";
  21.133 -val thy_goal = kind "thy_goal";
  21.134 -val qed = kind "qed";
  21.135 -val qed_script = kind "qed_script";
  21.136 -val qed_block = kind "qed_block";
  21.137 -val qed_global = kind "qed_global";
  21.138 -val prf_goal = kind "prf_goal";
  21.139 -val prf_block = kind "prf_block";
  21.140 -val prf_open = kind "prf_open";
  21.141 -val prf_close = kind "prf_close";
  21.142 -val prf_chain = kind "prf_chain";
  21.143 -val prf_decl = kind "prf_decl";
  21.144 -val prf_asm = kind "prf_asm";
  21.145 -val prf_asm_goal = kind "prf_asm_goal";
  21.146 -val prf_asm_goal_script = kind "prf_asm_goal_script";
  21.147 -val prf_script = kind "prf_script";
  21.148 -
  21.149 -val kinds =
  21.150 -  [diag, heading, thy_begin, thy_end, thy_load, thy_decl, thy_decl_block, thy_goal,
  21.151 -    qed, qed_script, qed_block, qed_global, prf_goal, prf_block, prf_open, prf_close,
  21.152 -    prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_asm_goal_script, prf_script]
  21.153 -  |> map kind_of;
  21.154 -
  21.155 -
  21.156 -(* specifications *)
  21.157 -
  21.158  type spec = (string * string list) * string list;
  21.159  
  21.160 -fun check_spec ((kind, files), tags) =
  21.161 +fun check_spec ((kind, files), tags) : T =
  21.162    if not (member (op =) kinds kind) then
  21.163      error ("Unknown outer syntax keyword kind " ^ quote kind)
  21.164 -  else if not (null files) andalso kind <> kind_of thy_load then
  21.165 +  else if not (null files) andalso kind <> thy_load then
  21.166      error ("Illegal specification of files for " ^ quote kind)
  21.167 -  else Keyword {kind = kind, files = files, tags = tags};
  21.168 -
  21.169 -fun command_spec ((name, s), pos) = ((name, check_spec s), pos);
  21.170 +  else {kind = kind, files = files, tags = tags};
  21.171  
  21.172  
  21.173  
  21.174 @@ -158,41 +144,45 @@
  21.175      Scan.merge_lexicons (major1, major2),
  21.176      Symtab.merge (K true) (commands1, commands2));
  21.177  
  21.178 -fun add_keywords (name, opt_kind) = map_keywords (fn (minor, major, commands) =>
  21.179 -  (case opt_kind of
  21.180 -    NONE =>
  21.181 -      let
  21.182 -        val minor' = Scan.extend_lexicon (Symbol.explode name) minor;
  21.183 -      in (minor', major, commands) end
  21.184 -  | SOME kind =>
  21.185 -      let
  21.186 -        val major' = Scan.extend_lexicon (Symbol.explode name) major;
  21.187 -        val commands' = Symtab.update (name, kind) commands;
  21.188 -      in (minor, major', commands') end));
  21.189 +val add_keywords =
  21.190 +  fold (fn (name, opt_spec) => map_keywords (fn (minor, major, commands) =>
  21.191 +    (case opt_spec of
  21.192 +      NONE =>
  21.193 +        let
  21.194 +          val minor' = Scan.extend_lexicon (Symbol.explode name) minor;
  21.195 +        in (minor', major, commands) end
  21.196 +    | SOME spec =>
  21.197 +        let
  21.198 +          val kind = check_spec spec;
  21.199 +          val major' = Scan.extend_lexicon (Symbol.explode name) major;
  21.200 +          val commands' = Symtab.update (name, kind) commands;
  21.201 +        in (minor, major', commands') end)));
  21.202  
  21.203  
  21.204 -(* lookup *)
  21.205 +(* lookup keywords *)
  21.206  
  21.207 -fun is_keyword keywords s =
  21.208 +fun is_literal keywords s =
  21.209    let
  21.210      val minor = minor_keywords keywords;
  21.211      val major = major_keywords keywords;
  21.212      val syms = Symbol.explode s;
  21.213    in Scan.is_literal minor syms orelse Scan.is_literal major syms end;
  21.214  
  21.215 +fun is_command (Keywords {commands, ...}) = Symtab.defined commands;
  21.216 +
  21.217  fun command_keyword (Keywords {commands, ...}) = Symtab.lookup commands;
  21.218  
  21.219  fun command_files keywords name path =
  21.220    (case command_keyword keywords name of
  21.221      NONE => []
  21.222 -  | SOME (Keyword {kind, files, ...}) =>
  21.223 -      if kind <> kind_of thy_load then []
  21.224 +  | SOME {kind, files, ...} =>
  21.225 +      if kind <> thy_load then []
  21.226        else if null files then [path]
  21.227        else map (fn ext => Path.ext ext path) files);
  21.228  
  21.229  fun command_tags keywords name =
  21.230    (case command_keyword keywords name of
  21.231 -    SOME (Keyword {tags, ...}) => tags
  21.232 +    SOME {tags, ...} => tags
  21.233    | NONE => []);
  21.234  
  21.235  
  21.236 @@ -200,11 +190,11 @@
  21.237  
  21.238  fun command_category ks =
  21.239    let
  21.240 -    val tab = Symtab.make_set (map kind_of ks);
  21.241 +    val tab = Symtab.make_set ks;
  21.242      fun pred keywords name =
  21.243        (case command_keyword keywords name of
  21.244          NONE => false
  21.245 -      | SOME k => Symtab.defined tab (kind_of k));
  21.246 +      | SOME {kind, ...} => Symtab.defined tab kind);
  21.247    in pred end;
  21.248  
  21.249  val is_diag = command_category [diag];
  21.250 @@ -236,16 +226,5 @@
  21.251  
  21.252  fun is_printed keywords = is_theory_goal keywords orf is_proof keywords;
  21.253  
  21.254 -
  21.255 -
  21.256 -(** global state **)
  21.257 -
  21.258 -local val global_keywords = Unsynchronized.ref empty_keywords in
  21.259 -
  21.260 -fun define decl = CRITICAL (fn () => Unsynchronized.change global_keywords (add_keywords decl));
  21.261 -fun get_keywords () = ! global_keywords;
  21.262 -
  21.263  end;
  21.264  
  21.265 -end;
  21.266 -
    22.1 --- a/src/Pure/Isar/keyword.scala	Fri Nov 07 16:22:25 2014 +0100
    22.2 +++ b/src/Pure/Isar/keyword.scala	Fri Nov 07 16:36:55 2014 +0100
    22.3 @@ -63,12 +63,11 @@
    22.4    val qed_global = Set(QED_GLOBAL)
    22.5  
    22.6  
    22.7 -  type Spec = ((String, List[String]), List[String])
    22.8 -
    22.9 -
   22.10  
   22.11    /** keyword tables **/
   22.12  
   22.13 +  type Spec = ((String, List[String]), List[String])
   22.14 +
   22.15    object Keywords
   22.16    {
   22.17      def empty: Keywords = new Keywords()
   22.18 @@ -99,13 +98,21 @@
   22.19  
   22.20      def + (name: String): Keywords = new Keywords(minor + name, major, commands)
   22.21      def + (name: String, kind: String): Keywords = this + (name, (kind, Nil))
   22.22 -    def + (name: String, kind: (String, List[String])): Keywords =
   22.23 +    def + (name: String, kind_tags: (String, List[String])): Keywords =
   22.24      {
   22.25        val major1 = major + name
   22.26 -      val commands1 = commands + (name -> kind)
   22.27 +      val commands1 = commands + (name -> kind_tags)
   22.28        new Keywords(minor, major1, commands1)
   22.29      }
   22.30  
   22.31 +    def add_keywords(header: Thy_Header.Keywords): Keywords =
   22.32 +      (this /: header) {
   22.33 +        case (keywords, (name, None, _)) =>
   22.34 +          keywords + Symbol.decode(name) + Symbol.encode(name)
   22.35 +        case (keywords, (name, Some((kind_tags, _)), _)) =>
   22.36 +          keywords + (Symbol.decode(name), kind_tags) + (Symbol.encode(name), kind_tags)
   22.37 +      }
   22.38 +
   22.39  
   22.40      /* command kind */
   22.41  
    23.1 --- a/src/Pure/Isar/outer_syntax.ML	Fri Nov 07 16:22:25 2014 +0100
    23.2 +++ b/src/Pure/Isar/outer_syntax.ML	Fri Nov 07 16:36:55 2014 +0100
    23.3 @@ -1,23 +1,19 @@
    23.4  (*  Title:      Pure/Isar/outer_syntax.ML
    23.5      Author:     Markus Wenzel, TU Muenchen
    23.6  
    23.7 -The global Isabelle/Isar outer syntax.
    23.8 -
    23.9 -Note: the syntax for files is statically determined at the very
   23.10 -beginning; for interactive processing it may change dynamically.
   23.11 +Isabelle/Isar outer syntax.
   23.12  *)
   23.13  
   23.14  signature OUTER_SYNTAX =
   23.15  sig
   23.16 -  type syntax
   23.17 -  val batch_mode: bool Unsynchronized.ref
   23.18 -  val is_markup: syntax -> Thy_Output.markup -> string -> bool
   23.19 -  val get_syntax: unit -> Keyword.keywords * syntax
   23.20 -  val check_syntax: unit -> unit
   23.21 -  type command_spec = (string * Keyword.T) * Position.T
   23.22 +  datatype markup = Markup | Markup_Env | Verbatim
   23.23 +  val is_markup: theory -> markup -> string -> bool
   23.24 +  val help_syntax: theory -> string list -> unit
   23.25 +  val print_syntax: theory -> unit
   23.26 +  type command_spec = string * Position.T
   23.27    val command: command_spec -> string ->
   23.28      (Toplevel.transition -> Toplevel.transition) parser -> unit
   23.29 -  val markup_command: Thy_Output.markup -> command_spec -> string ->
   23.30 +  val markup_command: markup -> command_spec -> string ->
   23.31      (Toplevel.transition -> Toplevel.transition) parser -> unit
   23.32    val local_theory': command_spec -> string ->
   23.33      (bool -> local_theory -> local_theory) parser -> unit
   23.34 @@ -27,14 +23,12 @@
   23.35      (bool -> local_theory -> Proof.state) parser -> unit
   23.36    val local_theory_to_proof: command_spec -> string ->
   23.37      (local_theory -> Proof.state) parser -> unit
   23.38 -  val help_syntax: string list -> unit
   23.39 -  val print_syntax: unit -> unit
   23.40    val scan: Keyword.keywords -> Position.T -> string -> Token.T list
   23.41 -  val parse: Keyword.keywords * syntax -> Position.T -> string -> Toplevel.transition list
   23.42 +  val parse: theory -> Position.T -> string -> Toplevel.transition list
   23.43 +  val parse_tokens: theory -> Token.T list -> Toplevel.transition list
   23.44    val parse_spans: Token.T list -> Command_Span.span list
   23.45    val side_comments: Token.T list -> Token.T list
   23.46 -  val command_reports: syntax -> Token.T -> Position.report_text list
   23.47 -  val read_spans: syntax -> Token.T list -> Toplevel.transition list
   23.48 +  val command_reports: theory -> Token.T -> Position.report_text list
   23.49  end;
   23.50  
   23.51  structure Outer_Syntax: OUTER_SYNTAX =
   23.52 @@ -42,18 +36,33 @@
   23.53  
   23.54  (** outer syntax **)
   23.55  
   23.56 +(* errors *)
   23.57 +
   23.58 +fun err_command msg name ps =
   23.59 +  error (msg ^ quote (Markup.markup Markup.keyword1 name) ^ Position.here_list ps);
   23.60 +
   23.61 +fun err_dup_command name ps =
   23.62 +  err_command "Duplicate outer syntax command " name ps;
   23.63 +
   23.64 +
   23.65  (* command parsers *)
   23.66  
   23.67 +datatype markup = Markup | Markup_Env | Verbatim;
   23.68 +
   23.69  datatype command = Command of
   23.70   {comment: string,
   23.71 -  markup: Thy_Output.markup option,
   23.72 +  markup: markup option,
   23.73    parse: (Toplevel.transition -> Toplevel.transition) parser,
   23.74    pos: Position.T,
   23.75    id: serial};
   23.76  
   23.77 +fun eq_command (Command {id = id1, ...}, Command {id = id2, ...}) = id1 = id2;
   23.78 +
   23.79  fun new_command comment markup parse pos =
   23.80    Command {comment = comment, markup = markup, parse = parse, pos = pos, id = serial ()};
   23.81  
   23.82 +fun command_pos (Command {pos, ...}) = pos;
   23.83 +
   23.84  fun command_markup def (name, Command {pos, id, ...}) =
   23.85    Markup.properties (Position.entity_properties_of def id pos)
   23.86      (Markup.entity Markup.commandN name);
   23.87 @@ -69,94 +78,104 @@
   23.88  
   23.89  datatype syntax = Syntax of
   23.90   {commands: command Symtab.table,
   23.91 -  markups: (string * Thy_Output.markup) list};
   23.92 +  markups: (string * markup) list};
   23.93  
   23.94 -fun make_syntax commands markups =
   23.95 +fun make_syntax (commands, markups) =
   23.96    Syntax {commands = commands, markups = markups};
   23.97  
   23.98 -val empty_syntax = make_syntax Symtab.empty [];
   23.99 +structure Data = Theory_Data
  23.100 +(
  23.101 +  type T = syntax;
  23.102 +  val empty = make_syntax (Symtab.empty, []);
  23.103 +  val extend = I;
  23.104 +  fun merge (Syntax {commands = commands1, markups = markups1},
  23.105 +      Syntax {commands = commands2, markups = markups2}) =
  23.106 +    let
  23.107 +      val commands' = (commands1, commands2)
  23.108 +        |> Symtab.join (fn name => fn (cmd1, cmd2) =>
  23.109 +          if eq_command (cmd1, cmd2) then raise Symtab.SAME
  23.110 +          else err_dup_command name [command_pos cmd1, command_pos cmd2]);
  23.111 +      val markups' = AList.merge (op =) (K true) (markups1, markups2);
  23.112 +    in make_syntax (commands', markups') end;
  23.113 +);
  23.114  
  23.115  
  23.116 -fun map_commands f (Syntax {commands, ...}) =
  23.117 +(* inspect syntax *)
  23.118 +
  23.119 +val get_syntax = Data.get;
  23.120 +
  23.121 +val dest_commands =
  23.122 +  get_syntax #> (fn Syntax {commands, ...} => commands |> Symtab.dest |> sort_wrt #1);
  23.123 +
  23.124 +val lookup_commands =
  23.125 +  get_syntax #> (fn Syntax {commands, ...} => Symtab.lookup commands);
  23.126 +
  23.127 +val is_markup =
  23.128 +  get_syntax #> (fn Syntax {markups, ...} => fn kind => fn name =>
  23.129 +    AList.lookup (op =) markups name = SOME kind);
  23.130 +
  23.131 +fun help_syntax thy pats =
  23.132 +  dest_commands thy
  23.133 +  |> filter (fn (name, _) => forall (fn pat => match_string pat name) pats)
  23.134 +  |> map pretty_command
  23.135 +  |> Pretty.writeln_chunks;
  23.136 +
  23.137 +fun print_syntax thy =
  23.138    let
  23.139 -    val commands' = f commands;
  23.140 +    val keywords = Thy_Header.get_keywords thy;
  23.141 +    val minor = Scan.dest_lexicon (Keyword.minor_keywords keywords);
  23.142 +    val commands = dest_commands thy;
  23.143 +  in
  23.144 +    [Pretty.strs ("keywords:" :: map quote minor),
  23.145 +      Pretty.big_list "commands:" (map pretty_command commands)]
  23.146 +    |> Pretty.writeln_chunks
  23.147 +  end;
  23.148 +
  23.149 +
  23.150 +(* build syntax *)
  23.151 +
  23.152 +fun add_command name cmd thy = thy |> Data.map (fn Syntax {commands, ...} =>
  23.153 +  let
  23.154 +    val keywords = Thy_Header.get_keywords thy;
  23.155 +    val _ =
  23.156 +      Keyword.is_command keywords name orelse
  23.157 +        err_command "Undeclared outer syntax command " name [command_pos cmd];
  23.158 +
  23.159 +    val _ =
  23.160 +      (case Symtab.lookup commands name of
  23.161 +        NONE => ()
  23.162 +      | SOME cmd' => err_dup_command name [command_pos cmd, command_pos cmd']);
  23.163 +
  23.164 +    val _ =
  23.165 +      Context_Position.report_generic (ML_Context.the_generic_context ())
  23.166 +        (command_pos cmd) (command_markup true (name, cmd));
  23.167 +
  23.168 +    val commands' = Symtab.update (name, cmd) commands;
  23.169      val markups' =
  23.170        Symtab.fold (fn (name, Command {markup = SOME m, ...}) => cons (name, m) | _ => I)
  23.171          commands' [];
  23.172 -  in make_syntax commands' markups' end;
  23.173 -
  23.174 -fun dest_commands (Syntax {commands, ...}) =
  23.175 -  commands |> Symtab.dest |> sort_wrt #1;
  23.176 +  in make_syntax (commands', markups') end);
  23.177  
  23.178 -fun lookup_commands (Syntax {commands, ...}) = Symtab.lookup commands;
  23.179 -
  23.180 -fun is_markup (Syntax {markups, ...}) kind name =
  23.181 -  AList.lookup (op =) markups name = SOME kind;
  23.182 -
  23.183 +val _ = Theory.setup (Theory.at_end (fn thy =>
  23.184 +  let
  23.185 +    val keywords = Thy_Header.get_keywords thy;
  23.186 +    val major = Keyword.major_keywords keywords;
  23.187 +    val _ =
  23.188 +      (case subtract (op =) (map #1 (dest_commands thy)) (Scan.dest_lexicon major) of
  23.189 +        [] => ()
  23.190 +      | missing => error ("Missing outer syntax command(s) " ^ commas_quote missing))
  23.191 +  in NONE end));
  23.192  
  23.193  
  23.194 -(** global outer syntax **)
  23.195 -
  23.196 -type command_spec = (string * Keyword.T) * Position.T;
  23.197 +(* implicit theory setup *)
  23.198  
  23.199 -val batch_mode = Unsynchronized.ref false;
  23.200 -
  23.201 -local
  23.202 -
  23.203 -(*synchronized wrt. Keywords*)
  23.204 -val global_syntax = Unsynchronized.ref empty_syntax;
  23.205 +type command_spec = string * Position.T;
  23.206  
  23.207 -fun add_command (name, kind) cmd = CRITICAL (fn () =>
  23.208 -  let
  23.209 -    val context = ML_Context.the_generic_context ();
  23.210 -    val thy = Context.theory_of context;
  23.211 -    val Command {pos, ...} = cmd;
  23.212 -    val command_name = quote (Markup.markup Markup.keyword1 name);
  23.213 -    val _ =
  23.214 -      (case try (Thy_Header.the_keyword thy) name of
  23.215 -        SOME spec =>
  23.216 -          if Option.map #1 spec = SOME (Keyword.kind_files_of kind) then ()
  23.217 -          else
  23.218 -            error ("Inconsistent outer syntax keyword declaration " ^
  23.219 -              command_name ^ Position.here pos)
  23.220 -      | NONE =>
  23.221 -          error ("Undeclared outer syntax command " ^ command_name ^ Position.here pos));
  23.222 -    val _ = Context_Position.report_generic context pos (command_markup true (name, cmd));
  23.223 -  in
  23.224 -    Unsynchronized.change global_syntax (map_commands (fn commands =>
  23.225 -     (if not (Symtab.defined commands name) then ()
  23.226 -      else if ! batch_mode then
  23.227 -        error ("Attempt to redefine outer syntax command " ^ command_name)
  23.228 -      else
  23.229 -        warning ("Redefining outer syntax command " ^ command_name ^
  23.230 -          Position.here (Position.thread_data ()));
  23.231 -      Symtab.update (name, cmd) commands)))
  23.232 -  end);
  23.233 +fun command (name, pos) comment parse =
  23.234 +  Theory.setup (add_command name (new_command comment NONE parse pos));
  23.235  
  23.236 -in
  23.237 -
  23.238 -fun get_syntax () = CRITICAL (fn () => (Keyword.get_keywords (), ! global_syntax));
  23.239 -
  23.240 -fun check_syntax () =
  23.241 -  let
  23.242 -    val (keywords, syntax) = CRITICAL (fn () => (Keyword.get_keywords (), ! global_syntax));
  23.243 -    val major = Keyword.major_keywords keywords;
  23.244 -  in
  23.245 -    (case subtract (op =) (map #1 (dest_commands syntax)) (Scan.dest_lexicon major) of
  23.246 -      [] => ()
  23.247 -    | missing => error ("Missing outer syntax command(s) " ^ commas_quote missing))
  23.248 -  end;
  23.249 -
  23.250 -fun command (spec, pos) comment parse =
  23.251 -  add_command spec (new_command comment NONE parse pos);
  23.252 -
  23.253 -fun markup_command markup (spec, pos) comment parse =
  23.254 -  add_command spec (new_command comment (SOME markup) parse pos);
  23.255 -
  23.256 -end;
  23.257 -
  23.258 -
  23.259 -(* local_theory commands *)
  23.260 +fun markup_command markup (name, pos) comment parse =
  23.261 +  Theory.setup (add_command name (new_command comment (SOME markup) parse pos));
  23.262  
  23.263  fun local_theory_command trans command_spec comment parse =
  23.264    command command_spec comment (Parse.opt_target -- parse >> (fn (loc, f) => trans loc f));
  23.265 @@ -167,60 +186,10 @@
  23.266  val local_theory_to_proof = local_theory_command Toplevel.local_theory_to_proof;
  23.267  
  23.268  
  23.269 -(* inspect syntax *)
  23.270 -
  23.271 -fun help_syntax pats =
  23.272 -  dest_commands (#2 (get_syntax ()))
  23.273 -  |> filter (fn (name, _) => forall (fn pat => match_string pat name) pats)
  23.274 -  |> map pretty_command
  23.275 -  |> Pretty.writeln_chunks;
  23.276 -
  23.277 -fun print_syntax () =
  23.278 -  let
  23.279 -    val (keywords, syntax) = CRITICAL (fn () => (Keyword.get_keywords (), #2 (get_syntax ())));
  23.280 -    val minor = Scan.dest_lexicon (Keyword.minor_keywords keywords);
  23.281 -    val commands = dest_commands syntax;
  23.282 -  in
  23.283 -    [Pretty.strs ("keywords:" :: map quote minor),
  23.284 -      Pretty.big_list "commands:" (map pretty_command commands)]
  23.285 -    |> Pretty.writeln_chunks
  23.286 -  end;
  23.287 -
  23.288 -
  23.289  
  23.290  (** toplevel parsing **)
  23.291  
  23.292 -(* parse commands *)
  23.293 -
  23.294 -local
  23.295 -
  23.296 -fun parse_command syntax =
  23.297 -  Parse.position Parse.command_ :|-- (fn (name, pos) =>
  23.298 -    let
  23.299 -      val tr0 = Toplevel.empty |> Toplevel.name name |> Toplevel.position pos;
  23.300 -    in
  23.301 -      (case lookup_commands syntax name of
  23.302 -        SOME (Command {parse, ...}) => Parse.!!! (Parse.tags |-- parse) >> (fn f => f tr0)
  23.303 -      | NONE =>
  23.304 -          Scan.succeed
  23.305 -            (tr0 |> Toplevel.imperative (fn () =>
  23.306 -              error ("Bad parser for outer syntax command " ^ quote name ^ Position.here pos))))
  23.307 -    end);
  23.308 -
  23.309 -val parse_cmt = Parse.$$$ "--" -- Parse.!!! Parse.document_source;
  23.310 -
  23.311 -in
  23.312 -
  23.313 -fun commands_source syntax =
  23.314 -  Token.source_proper #>
  23.315 -  Source.source Token.stopper (Scan.bulk (parse_cmt >> K NONE || Parse.not_eof >> SOME)) #>
  23.316 -  Source.map_filter I #>
  23.317 -  Source.source Token.stopper (Scan.bulk (fn xs => Parse.!!! (parse_command syntax) xs));
  23.318 -
  23.319 -end;
  23.320 -
  23.321 -
  23.322 -(* off-line scanning/parsing *)
  23.323 +(* scan tokens *)
  23.324  
  23.325  fun scan keywords pos =
  23.326    Source.of_string #>
  23.327 @@ -228,11 +197,46 @@
  23.328    Token.source keywords pos #>
  23.329    Source.exhaust;
  23.330  
  23.331 -fun parse (keywords, syntax) pos str =
  23.332 +
  23.333 +(* parse commands *)
  23.334 +
  23.335 +local
  23.336 +
  23.337 +fun parse_command thy =
  23.338 +  Parse.position Parse.command_ :|-- (fn (name, pos) =>
  23.339 +    let
  23.340 +      val tr0 = Toplevel.empty |> Toplevel.name name |> Toplevel.position pos;
  23.341 +    in
  23.342 +      (case lookup_commands thy name of
  23.343 +        SOME (Command {parse, ...}) => Parse.!!! (Parse.tags |-- parse) >> (fn f => f tr0)
  23.344 +      | NONE =>
  23.345 +          Scan.succeed
  23.346 +            (tr0 |> Toplevel.imperative (fn () =>
  23.347 +              err_command "Bad parser for outer syntax command " name [pos])))
  23.348 +    end);
  23.349 +
  23.350 +val parse_cmt = Parse.$$$ "--" -- Parse.!!! Parse.document_source;
  23.351 +
  23.352 +in
  23.353 +
  23.354 +fun commands_source thy =
  23.355 +  Token.source_proper #>
  23.356 +  Source.source Token.stopper (Scan.bulk (parse_cmt >> K NONE || Parse.not_eof >> SOME)) #>
  23.357 +  Source.map_filter I #>
  23.358 +  Source.source Token.stopper (Scan.bulk (fn xs => Parse.!!! (parse_command thy) xs));
  23.359 +
  23.360 +end;
  23.361 +
  23.362 +fun parse thy pos str =
  23.363    Source.of_string str
  23.364    |> Symbol.source
  23.365 -  |> Token.source keywords pos
  23.366 -  |> commands_source syntax
  23.367 +  |> Token.source (Thy_Header.get_keywords thy) pos
  23.368 +  |> commands_source thy
  23.369 +  |> Source.exhaust;
  23.370 +
  23.371 +fun parse_tokens thy toks =
  23.372 +  Source.of_list toks
  23.373 +  |> commands_source thy
  23.374    |> Source.exhaust;
  23.375  
  23.376  
  23.377 @@ -279,19 +283,14 @@
  23.378  
  23.379  (* read commands *)
  23.380  
  23.381 -fun command_reports syntax tok =
  23.382 +fun command_reports thy tok =
  23.383    if Token.is_command tok then
  23.384      let val name = Token.content_of tok in
  23.385 -      (case lookup_commands syntax name of
  23.386 +      (case lookup_commands thy name of
  23.387          NONE => []
  23.388        | SOME cmd => [((Token.pos_of tok, command_markup false (name, cmd)), "")])
  23.389      end
  23.390    else [];
  23.391  
  23.392 -fun read_spans syntax toks =
  23.393 -  Source.of_list toks
  23.394 -  |> commands_source syntax
  23.395 -  |> Source.exhaust;
  23.396 -
  23.397  end;
  23.398  
    24.1 --- a/src/Pure/ML/ml_antiquotations.ML	Fri Nov 07 16:22:25 2014 +0100
    24.2 +++ b/src/Pure/ML/ml_antiquotations.ML	Fri Nov 07 16:36:55 2014 +0100
    24.3 @@ -234,29 +234,19 @@
    24.4  (* outer syntax *)
    24.5  
    24.6  fun with_keyword f =
    24.7 -  Args.theory -- Scan.lift (Parse.position Parse.string) >> (fn (thy, (name, pos)) =>
    24.8 -    (f ((name, Thy_Header.the_keyword thy name), pos)
    24.9 -      handle ERROR msg => error (msg ^ Position.here pos)));
   24.10 +  Args.theory -- Scan.lift (Parse.position Parse.string)
   24.11 +    >> (fn (thy, (name, pos)) => (f (name, pos, Thy_Header.the_keyword thy (name, pos))));
   24.12  
   24.13  val _ = Theory.setup
   24.14   (ML_Antiquotation.value @{binding keyword}
   24.15 -    (with_keyword
   24.16 -      (fn ((name, NONE), _) => "Parse.$$$ " ^ ML_Syntax.print_string name
   24.17 -        | ((name, SOME _), pos) =>
   24.18 -            error ("Expected minor keyword " ^ quote name ^ Position.here pos))) #>
   24.19 +    (with_keyword (fn (name, pos, is_command) =>
   24.20 +      if not is_command then "Parse.$$$ " ^ ML_Syntax.print_string name
   24.21 +      else error ("Expected minor keyword " ^ quote name ^ Position.here pos))) #>
   24.22    ML_Antiquotation.value @{binding command_spec}
   24.23 -    (with_keyword
   24.24 -      (fn ((name, SOME kind), pos) =>
   24.25 -          "Keyword.command_spec " ^ ML_Syntax.atomic
   24.26 -            ((ML_Syntax.print_pair
   24.27 -              (ML_Syntax.print_pair ML_Syntax.print_string
   24.28 -                (ML_Syntax.print_pair
   24.29 -                  (ML_Syntax.print_pair ML_Syntax.print_string
   24.30 -                    (ML_Syntax.print_list ML_Syntax.print_string))
   24.31 -                  (ML_Syntax.print_list ML_Syntax.print_string)))
   24.32 -              ML_Syntax.print_position) ((name, kind), pos))
   24.33 -        | ((name, NONE), pos) =>
   24.34 -            error ("Expected command keyword " ^ quote name ^ Position.here pos))));
   24.35 +    (with_keyword (fn (name, pos, is_command) =>
   24.36 +      if is_command then
   24.37 +        ML_Syntax.print_pair ML_Syntax.print_string ML_Syntax.print_position (name, pos)
   24.38 +      else error ("Expected command keyword " ^ quote name ^ Position.here pos))));
   24.39  
   24.40  end;
   24.41  
    25.1 --- a/src/Pure/ML/ml_context.ML	Fri Nov 07 16:22:25 2014 +0100
    25.2 +++ b/src/Pure/ML/ml_context.ML	Fri Nov 07 16:36:55 2014 +0100
    25.3 @@ -116,12 +116,12 @@
    25.4        then ((begin_env0, map (fn Antiquote.Text tok => tok) ants), opt_ctxt)
    25.5        else
    25.6          let
    25.7 -          val keywords = Keyword.get_keywords ();
    25.8            fun no_decl _ = ([], []);
    25.9  
   25.10            fun expand (Antiquote.Text tok) ctxt = (K ([], [tok]), ctxt)
   25.11              | expand (Antiquote.Antiq (ss, {range, ...})) ctxt =
   25.12                  let
   25.13 +                  val keywords = Thy_Header.get_keywords' ctxt;
   25.14                    val (decl, ctxt') =
   25.15                      apply_antiquotation (Token.read_antiq keywords antiq (ss, #1 range)) ctxt;
   25.16                    val decl' = decl #> pairself (ML_Lex.tokenize #> map (ML_Lex.set_range range));
    26.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    26.2 +++ b/src/Pure/ML/ml_file.ML	Fri Nov 07 16:36:55 2014 +0100
    26.3 @@ -0,0 +1,25 @@
    26.4 +(*  Title:      Pure/ML/ml_file.ML
    26.5 +    Author:     Makarius
    26.6 +
    26.7 +The 'ML_file' command.
    26.8 +*)
    26.9 +
   26.10 +structure ML_File: sig end =
   26.11 +struct
   26.12 +
   26.13 +val _ =
   26.14 +  Outer_Syntax.command ("ML_file", @{here}) "ML text from file"
   26.15 +    (Resources.parse_files "ML_file" >> (fn files => Toplevel.generic_theory (fn gthy =>
   26.16 +        let
   26.17 +          val [{src_path, lines, digest, pos}] = files (Context.theory_of gthy);
   26.18 +          val provide = Resources.provide (src_path, digest);
   26.19 +          val source = {delimited = true, text = cat_lines lines, pos = pos};
   26.20 +          val flags = {SML = false, exchange = false, redirect = true, verbose = true};
   26.21 +        in
   26.22 +          gthy
   26.23 +          |> ML_Context.exec (fn () => ML_Context.eval_source flags source)
   26.24 +          |> Local_Theory.propagate_ml_env
   26.25 +          |> Context.mapping provide (Local_Theory.background_theory provide)
   26.26 +        end)));
   26.27 +
   26.28 +end;
    27.1 --- a/src/Pure/PIDE/command.ML	Fri Nov 07 16:22:25 2014 +0100
    27.2 +++ b/src/Pure/PIDE/command.ML	Fri Nov 07 16:36:55 2014 +0100
    27.3 @@ -8,15 +8,15 @@
    27.4  sig
    27.5    type blob = (string * (SHA1.digest * string list) option) Exn.result
    27.6    val read_file: Path.T -> Position.T -> Path.T -> Token.file
    27.7 -  val read: Keyword.keywords -> Path.T-> (unit -> theory) -> blob list -> Token.T list ->
    27.8 +  val read_thy: Toplevel.state -> theory
    27.9 +  val read: theory -> Path.T-> (unit -> theory) -> blob list -> Token.T list ->
   27.10      Toplevel.transition
   27.11    type eval
   27.12    val eval_eq: eval * eval -> bool
   27.13    val eval_running: eval -> bool
   27.14    val eval_finished: eval -> bool
   27.15    val eval_result_state: eval -> Toplevel.state
   27.16 -  val eval: Keyword.keywords -> Path.T -> (unit -> theory) -> blob list -> Token.T list ->
   27.17 -    eval -> eval
   27.18 +  val eval: Path.T -> (unit -> theory) -> blob list -> Token.T list -> eval -> eval
   27.19    type print
   27.20    val print: bool -> (string * string list) list -> Keyword.keywords -> string ->
   27.21      eval -> print list -> print list option
   27.22 @@ -145,12 +145,16 @@
   27.23        |> Command_Span.content
   27.24    | _ => toks);
   27.25  
   27.26 +val bootstrap_thy = ML_Context.the_global_context ();
   27.27 +
   27.28  in
   27.29  
   27.30 -fun read keywords master_dir init blobs span =
   27.31 +fun read_thy st = Toplevel.theory_of st handle Toplevel.UNDEF => bootstrap_thy;
   27.32 +
   27.33 +fun read thy master_dir init blobs span =
   27.34    let
   27.35 -    val syntax = #2 (Outer_Syntax.get_syntax ());
   27.36 -    val command_reports = Outer_Syntax.command_reports syntax;
   27.37 +    val keywords = Thy_Header.get_keywords thy;
   27.38 +    val command_reports = Outer_Syntax.command_reports thy;
   27.39  
   27.40      val proper_range = Token.range_of (#1 (take_suffix Token.is_improper span));
   27.41      val pos =
   27.42 @@ -163,7 +167,7 @@
   27.43    in
   27.44      if is_malformed then Toplevel.malformed pos "Malformed command syntax"
   27.45      else
   27.46 -      (case Outer_Syntax.read_spans syntax (resolve_files keywords master_dir blobs span) of
   27.47 +      (case Outer_Syntax.parse_tokens thy (resolve_files keywords master_dir blobs span) of
   27.48          [tr] => Toplevel.modify_init init tr
   27.49        | [] => Toplevel.ignored (#1 (Token.range_of span))
   27.50        | _ => Toplevel.malformed (#1 proper_range) "Exactly one command expected")
   27.51 @@ -264,15 +268,17 @@
   27.52  
   27.53  in
   27.54  
   27.55 -fun eval keywords master_dir init blobs span eval0 =
   27.56 +fun eval master_dir init blobs span eval0 =
   27.57    let
   27.58      val exec_id = Document_ID.make ();
   27.59      fun process () =
   27.60        let
   27.61 +        val eval_state0 = eval_result eval0;
   27.62 +        val thy = read_thy (#state eval_state0);
   27.63          val tr =
   27.64            Position.setmp_thread_data (Position.id_only (Document_ID.print exec_id))
   27.65 -            (fn () => read keywords master_dir init blobs span |> Toplevel.exec_id exec_id) ();
   27.66 -      in eval_state keywords span tr (eval_result eval0) end;
   27.67 +            (fn () => read thy master_dir init blobs span |> Toplevel.exec_id exec_id) ();
   27.68 +      in eval_state (Thy_Header.get_keywords thy) span tr eval_state0 end;
   27.69    in Eval {exec_id = exec_id, eval_process = memo exec_id process} end;
   27.70  
   27.71  end;
    28.1 --- a/src/Pure/PIDE/document.ML	Fri Nov 07 16:22:25 2014 +0100
    28.2 +++ b/src/Pure/PIDE/document.ML	Fri Nov 07 16:36:55 2014 +0100
    28.3 @@ -8,6 +8,7 @@
    28.4  signature DOCUMENT =
    28.5  sig
    28.6    val timing: bool Unsynchronized.ref
    28.7 +  val init_keywords: unit -> unit
    28.8    type node_header = string * Thy_Header.header * string list
    28.9    type overlay = Document_ID.command * (string * string list)
   28.10    datatype node_edit =
   28.11 @@ -37,6 +38,20 @@
   28.12  
   28.13  
   28.14  
   28.15 +(** global keywords **)
   28.16 +
   28.17 +val global_keywords = Synchronized.var "global_keywords" Keyword.empty_keywords;
   28.18 +
   28.19 +fun init_keywords () =
   28.20 +  Synchronized.change global_keywords
   28.21 +    (fn _ =>
   28.22 +      fold (curry Keyword.merge_keywords o Thy_Header.get_keywords o Thy_Info.get_theory)
   28.23 +        (Thy_Info.get_names ()) Keyword.empty_keywords);
   28.24 +
   28.25 +fun get_keywords () = Synchronized.value global_keywords;
   28.26 +
   28.27 +
   28.28 +
   28.29  (** document structure **)
   28.30  
   28.31  fun err_dup kind id = error ("Duplicate " ^ kind ^ ": " ^ Document_ID.print id);
   28.32 @@ -208,7 +223,7 @@
   28.33          let
   28.34            val imports = map fst (#imports header);
   28.35            val errors1 =
   28.36 -            (Thy_Header.define_keywords (#keywords header); errors)
   28.37 +            (Synchronized.change global_keywords (Keyword.add_keywords (#keywords header)); errors)
   28.38                handle ERROR msg => errors @ [msg];
   28.39            val nodes1 = nodes
   28.40              |> default_node name
   28.41 @@ -318,7 +333,7 @@
   28.42        val span =
   28.43          Lazy.lazy (fn () =>
   28.44            Position.setmp_thread_data (Position.id_only id)
   28.45 -            (fn () => Outer_Syntax.scan (Keyword.get_keywords ()) (Position.id id) text) ());
   28.46 +            (fn () => Outer_Syntax.scan (get_keywords ()) (Position.id id) text) ());
   28.47        val _ =
   28.48          Position.setmp_thread_data (Position.id_only id)
   28.49            (fn () => Output.status (Markup.markup_only Markup.accepted)) ();
   28.50 @@ -529,7 +544,7 @@
   28.51        val span = Lazy.force span0;
   28.52  
   28.53        val eval' =
   28.54 -        Command.eval keywords (master_directory node)
   28.55 +        Command.eval (master_directory node)
   28.56            (fn () => the_default illegal_init init span) blobs span eval;
   28.57        val prints' =
   28.58          perhaps (Command.print command_visible command_overlays keywords command_name eval') [];
   28.59 @@ -562,7 +577,7 @@
   28.60                deps = map (Future.task_of o #2) deps, pri = 1, interrupts = false}
   28.61              (fn () => timeit ("Document.update " ^ name) (fn () =>
   28.62                let
   28.63 -                val keywords = Keyword.get_keywords ();
   28.64 +                val keywords = get_keywords ();
   28.65                  val imports = map (apsnd Future.join) deps;
   28.66                  val imports_result_changed = exists (#4 o #1 o #2) imports;
   28.67                  val node_required = Symtab.defined required name;
    29.1 --- a/src/Pure/PIDE/protocol.ML	Fri Nov 07 16:22:25 2014 +0100
    29.2 +++ b/src/Pure/PIDE/protocol.ML	Fri Nov 07 16:36:55 2014 +0100
    29.3 @@ -23,6 +23,10 @@
    29.4        end);
    29.5  
    29.6  val _ =
    29.7 +  Isabelle_Process.protocol_command "Document.init_keywords"
    29.8 +    (fn [] => Document.init_keywords ());
    29.9 +
   29.10 +val _ =
   29.11    Isabelle_Process.protocol_command "Document.define_blob"
   29.12      (fn [digest, content] => Document.change_state (Document.define_blob digest content));
   29.13  
    30.1 --- a/src/Pure/PIDE/resources.ML	Fri Nov 07 16:22:25 2014 +0100
    30.2 +++ b/src/Pure/PIDE/resources.ML	Fri Nov 07 16:36:55 2014 +0100
    30.3 @@ -82,7 +82,7 @@
    30.4      (case Token.get_files tok of
    30.5        [] =>
    30.6          let
    30.7 -          val keywords = Keyword.get_keywords ();
    30.8 +          val keywords = Thy_Header.get_keywords thy;
    30.9            val master_dir = master_directory thy;
   30.10            val pos = Token.pos_of tok;
   30.11            val src_paths = Keyword.command_files keywords cmd (Path.explode name);
   30.12 @@ -122,18 +122,18 @@
   30.13  fun begin_theory master_dir {name, imports, keywords} parents =
   30.14    Theory.begin_theory name parents
   30.15    |> put_deps master_dir imports
   30.16 -  |> fold Thy_Header.declare_keyword keywords;
   30.17 +  |> Thy_Header.add_keywords keywords;
   30.18  
   30.19  fun excursion keywords master_dir last_timing init elements =
   30.20    let
   30.21 -    fun prepare_span span =
   30.22 +    fun prepare_span st span =
   30.23        Command_Span.content span
   30.24 -      |> Command.read keywords master_dir init []
   30.25 +      |> Command.read (Command.read_thy st) master_dir init []
   30.26        |> (fn tr => Toplevel.put_timing (last_timing tr) tr);
   30.27  
   30.28      fun element_result span_elem (st, _) =
   30.29        let
   30.30 -        val elem = Thy_Syntax.map_element prepare_span span_elem;
   30.31 +        val elem = Thy_Syntax.map_element (prepare_span st) span_elem;
   30.32          val (results, st') = Toplevel.element_result keywords elem st;
   30.33          val pos' = Toplevel.pos_of (Thy_Syntax.last_element elem);
   30.34        in (results, (st', pos')) end;
   30.35 @@ -147,8 +147,9 @@
   30.36  fun load_thy document last_timing update_time master_dir header text_pos text parents =
   30.37    let
   30.38      val (name, _) = #name header;
   30.39 -    val _ = Thy_Header.define_keywords (#keywords header);
   30.40 -    val keywords = Keyword.get_keywords ();
   30.41 +    val keywords =
   30.42 +      fold (curry Keyword.merge_keywords o Thy_Header.get_keywords) parents
   30.43 +        (Keyword.add_keywords (#keywords header) Keyword.empty_keywords);
   30.44  
   30.45      val toks = Outer_Syntax.scan keywords text_pos text;
   30.46      val spans = Outer_Syntax.parse_spans toks;
   30.47 @@ -166,14 +167,11 @@
   30.48      fun present () =
   30.49        let
   30.50          val res = filter_out (Toplevel.is_ignored o #1) (maps Toplevel.join_results results);
   30.51 -        val (keywords, syntax) = Outer_Syntax.get_syntax ();
   30.52        in
   30.53          if exists (Toplevel.is_skipped_proof o #2) res then
   30.54            warning ("Cannot present theory with skipped proofs: " ^ quote name)
   30.55          else
   30.56 -          let val tex_source =
   30.57 -            Thy_Output.present_thy keywords (Outer_Syntax.is_markup syntax) res toks
   30.58 -            |> Buffer.content;
   30.59 +          let val tex_source = Thy_Output.present_thy thy res toks |> Buffer.content;
   30.60            in if document then Present.theory_output name tex_source else () end
   30.61        end;
   30.62  
    31.1 --- a/src/Pure/PIDE/session.ML	Fri Nov 07 16:22:25 2014 +0100
    31.2 +++ b/src/Pure/PIDE/session.ML	Fri Nov 07 16:36:55 2014 +0100
    31.3 @@ -54,7 +54,6 @@
    31.4   (Execution.shutdown ();
    31.5    Thy_Info.finish ();
    31.6    Present.finish ();
    31.7 -  Outer_Syntax.check_syntax ();
    31.8    Future.shutdown ();
    31.9    Event_Timer.shutdown ();
   31.10    Future.shutdown ();
    32.1 --- a/src/Pure/PIDE/session.scala	Fri Nov 07 16:22:25 2014 +0100
    32.2 +++ b/src/Pure/PIDE/session.scala	Fri Nov 07 16:36:55 2014 +0100
    32.3 @@ -610,6 +610,12 @@
    32.4    def update_options(options: Options)
    32.5    { manager.send_wait(Update_Options(options)) }
    32.6  
    32.7 +  def init_options(options: Options)
    32.8 +  {
    32.9 +    update_options(options)
   32.10 +    protocol_command("Document.init_keywords")
   32.11 +  }
   32.12 +
   32.13    def dialog_result(id: Document_ID.Generic, serial: Long, result: String)
   32.14    { manager.send(Session.Dialog_Result(id, serial, result)) }
   32.15  }
    33.1 --- a/src/Pure/Pure.thy	Fri Nov 07 16:22:25 2014 +0100
    33.2 +++ b/src/Pure/Pure.thy	Fri Nov 07 16:36:55 2014 +0100
    33.3 @@ -6,18 +6,12 @@
    33.4  
    33.5  theory Pure
    33.6    keywords
    33.7 -    "!!" "!" "%" "(" ")" "+" "," "--" ":" "::" ";" "<" "<=" "=" "=="
    33.8 -    "=>" "?" "[" "\<equiv>" "\<leftharpoondown>" "\<rightharpoonup>"
    33.9 -    "\<rightleftharpoons>" "\<subseteq>" "]" "and" "assumes"
   33.10 -    "attach" "begin" "binder" "constrains" "defines" "fixes" "for"
   33.11 -    "identifier" "if" "imports" "in" "includes" "infix" "infixl"
   33.12 -    "infixr" "is" "keywords" "notes" "obtains" "open" "output"
   33.13 +    "!!" "!" "+" "--" ":" ";" "<" "<=" "=" "=>" "?" "[" "\<equiv>"
   33.14 +    "\<leftharpoondown>" "\<rightharpoonup>" "\<rightleftharpoons>"
   33.15 +    "\<subseteq>" "]" "assumes" "attach" "binder" "constrains"
   33.16 +    "defines" "fixes" "for" "identifier" "if" "in" "includes" "infix"
   33.17 +    "infixl" "infixr" "is" "notes" "obtains" "open" "output"
   33.18      "overloaded" "pervasive" "shows" "structure" "unchecked" "where" "|"
   33.19 -  and "header" :: heading
   33.20 -  and "chapter" :: heading
   33.21 -  and "section" :: heading
   33.22 -  and "subsection" :: heading
   33.23 -  and "subsubsection" :: heading
   33.24    and "text" "text_raw" :: thy_decl
   33.25    and "txt" "txt_raw" :: prf_decl % "proof"
   33.26    and "default_sort" :: thy_decl == ""
    34.1 --- a/src/Pure/ROOT	Fri Nov 07 16:22:25 2014 +0100
    34.2 +++ b/src/Pure/ROOT	Fri Nov 07 16:36:55 2014 +0100
    34.3 @@ -154,6 +154,7 @@
    34.4      "ML/ml_compiler_polyml.ML"
    34.5      "ML/ml_context.ML"
    34.6      "ML/ml_env.ML"
    34.7 +    "ML/ml_file.ML"
    34.8      "ML/ml_lex.ML"
    34.9      "ML/ml_parse.ML"
   34.10      "ML/ml_options.ML"
    35.1 --- a/src/Pure/ROOT.ML	Fri Nov 07 16:22:25 2014 +0100
    35.2 +++ b/src/Pure/ROOT.ML	Fri Nov 07 16:36:55 2014 +0100
    35.3 @@ -302,10 +302,11 @@
    35.4  (*theory documents*)
    35.5  use "System/isabelle_system.ML";
    35.6  use "Thy/term_style.ML";
    35.7 +use "Isar/outer_syntax.ML";
    35.8  use "Thy/thy_output.ML";
    35.9 -use "Isar/outer_syntax.ML";
   35.10  use "General/graph_display.ML";
   35.11  use "Thy/present.ML";
   35.12 +use "pure_syn.ML";
   35.13  use "PIDE/command.ML";
   35.14  use "PIDE/query_operation.ML";
   35.15  use "PIDE/resources.ML";
   35.16 @@ -361,7 +362,7 @@
   35.17  
   35.18  (* the Pure theory *)
   35.19  
   35.20 -use "pure_syn.ML";
   35.21 +use "ML/ml_file.ML";
   35.22  Runtime.toplevel_program (fn () => Thy_Info.use_thy ("Pure", Position.none));
   35.23  Context.set_thread_data NONE;
   35.24  structure Pure = struct val thy = Thy_Info.get_theory "Pure" end;
    36.1 --- a/src/Pure/Thy/thy_header.ML	Fri Nov 07 16:22:25 2014 +0100
    36.2 +++ b/src/Pure/Thy/thy_header.ML	Fri Nov 07 16:36:55 2014 +0100
    36.3 @@ -12,9 +12,11 @@
    36.4      imports: (string * Position.T) list,
    36.5      keywords: keywords}
    36.6    val make: string * Position.T -> (string * Position.T) list -> keywords -> header
    36.7 -  val define_keywords: keywords -> unit
    36.8 -  val declare_keyword: string * Keyword.spec option -> theory -> theory
    36.9 -  val the_keyword: theory -> string -> Keyword.spec option
   36.10 +  val bootstrap_keywords: Keyword.keywords
   36.11 +  val add_keywords: keywords -> theory -> theory
   36.12 +  val get_keywords: theory -> Keyword.keywords
   36.13 +  val get_keywords': Proof.context -> Keyword.keywords
   36.14 +  val the_keyword: theory -> string * Position.T -> bool
   36.15    val args: header parser
   36.16    val read: Position.T -> string -> header
   36.17    val read_tokens: Token.T list -> header
   36.18 @@ -23,6 +25,10 @@
   36.19  structure Thy_Header: THY_HEADER =
   36.20  struct
   36.21  
   36.22 +(** keyword declarations **)
   36.23 +
   36.24 +(* header *)
   36.25 +
   36.26  type keywords = (string * Keyword.spec option) list;
   36.27  
   36.28  type header =
   36.29 @@ -34,37 +40,7 @@
   36.30    {name = name, imports = imports, keywords = keywords};
   36.31  
   36.32  
   36.33 -
   36.34 -(** keyword declarations **)
   36.35 -
   36.36 -fun define_keywords (keywords: keywords) =
   36.37 -  List.app (Keyword.define o apsnd (Option.map Keyword.check_spec)) keywords;
   36.38 -
   36.39 -fun err_dup name = error ("Duplicate declaration of outer syntax keyword " ^ quote name);
   36.40 -
   36.41 -structure Data = Theory_Data
   36.42 -(
   36.43 -  type T = Keyword.spec option Symtab.table;
   36.44 -  val empty = Symtab.empty;
   36.45 -  val extend = I;
   36.46 -  fun merge data : T = Symtab.merge (op =) data handle Symtab.DUP name => err_dup name;
   36.47 -);
   36.48 -
   36.49 -fun declare_keyword (name, spec) =
   36.50 -  Data.map (fn data =>
   36.51 -    (Option.map Keyword.check_spec spec;
   36.52 -      Symtab.update_new (name, spec) data handle Symtab.DUP dup => err_dup dup));
   36.53 -
   36.54 -fun the_keyword thy name =
   36.55 -  (case Symtab.lookup (Data.get thy) name of
   36.56 -    SOME spec => spec
   36.57 -  | NONE => error ("Undeclared outer syntax keyword " ^ quote name));
   36.58 -
   36.59 -
   36.60 -
   36.61 -(** concrete syntax **)
   36.62 -
   36.63 -(* header keywords *)
   36.64 +(* bootstrap keywords *)
   36.65  
   36.66  val headerN = "header";
   36.67  val chapterN = "chapter";
   36.68 @@ -77,18 +53,53 @@
   36.69  val keywordsN = "keywords";
   36.70  val beginN = "begin";
   36.71  
   36.72 -val header_keywords =
   36.73 +val bootstrap_keywords =
   36.74    Keyword.empty_keywords
   36.75 -  |> fold (Keyword.add_keywords o rpair NONE)
   36.76 -    ["%", "(", ")", ",", "::", "==", "and", beginN, importsN, keywordsN]
   36.77 -  |> fold Keyword.add_keywords
   36.78 -    [(headerN, SOME Keyword.heading),
   36.79 -     (chapterN, SOME Keyword.heading),
   36.80 -     (sectionN, SOME Keyword.heading),
   36.81 -     (subsectionN, SOME Keyword.heading),
   36.82 -     (subsubsectionN, SOME Keyword.heading),
   36.83 -     (theoryN, SOME Keyword.thy_begin)];
   36.84 +  |> Keyword.add_keywords
   36.85 +    [("%", NONE),
   36.86 +     ("(", NONE),
   36.87 +     (")", NONE),
   36.88 +     (",", NONE),
   36.89 +     ("::", NONE),
   36.90 +     ("==", NONE),
   36.91 +     ("and", NONE),
   36.92 +     (beginN, NONE),
   36.93 +     (importsN, NONE),
   36.94 +     (keywordsN, NONE),
   36.95 +     (headerN, SOME ((Keyword.heading, []), [])),
   36.96 +     (chapterN, SOME ((Keyword.heading, []), [])),
   36.97 +     (sectionN, SOME ((Keyword.heading, []), [])),
   36.98 +     (subsectionN, SOME ((Keyword.heading, []), [])),
   36.99 +     (subsubsectionN, SOME ((Keyword.heading, []), [])),
  36.100 +     (theoryN, SOME ((Keyword.thy_begin, []), ["theory"])),
  36.101 +     ("ML_file", SOME ((Keyword.thy_load, []), ["ML"]))];
  36.102 +
  36.103 +
  36.104 +(* theory data *)
  36.105  
  36.106 +structure Data = Theory_Data
  36.107 +(
  36.108 +  type T = Keyword.keywords;
  36.109 +  val empty = bootstrap_keywords;
  36.110 +  val extend = I;
  36.111 +  val merge = Keyword.merge_keywords;
  36.112 +);
  36.113 +
  36.114 +val add_keywords = Data.map o Keyword.add_keywords;
  36.115 +
  36.116 +val get_keywords = Data.get;
  36.117 +val get_keywords' = get_keywords o Proof_Context.theory_of;
  36.118 +
  36.119 +fun the_keyword thy (name, pos) =
  36.120 +  let val keywords = get_keywords thy in
  36.121 +    if Keyword.is_literal keywords name
  36.122 +    then Keyword.is_command keywords name
  36.123 +    else error ("Undeclared outer syntax keyword " ^ quote name ^ Position.here pos)
  36.124 +  end;
  36.125 +
  36.126 +
  36.127 +
  36.128 +(** concrete syntax **)
  36.129  
  36.130  (* header args *)
  36.131  
  36.132 @@ -145,7 +156,7 @@
  36.133    str
  36.134    |> Source.of_string_limited 8000
  36.135    |> Symbol.source
  36.136 -  |> Token.source_strict header_keywords pos;
  36.137 +  |> Token.source_strict bootstrap_keywords pos;
  36.138  
  36.139  fun read_source pos source =
  36.140    let val res =
    37.1 --- a/src/Pure/Thy/thy_header.scala	Fri Nov 07 16:22:25 2014 +0100
    37.2 +++ b/src/Pure/Thy/thy_header.scala	Fri Nov 07 16:36:55 2014 +0100
    37.3 @@ -15,6 +15,10 @@
    37.4  
    37.5  object Thy_Header extends Parse.Parser
    37.6  {
    37.7 +  /* bootstrap keywords */
    37.8 +
    37.9 +  type Keywords = List[(String, Option[Keyword.Spec], Option[String])]
   37.10 +
   37.11    val HEADER = "header"
   37.12    val CHAPTER = "chapter"
   37.13    val SECTION = "section"
   37.14 @@ -27,15 +31,31 @@
   37.15    val AND = "and"
   37.16    val BEGIN = "begin"
   37.17  
   37.18 -  private val header_keywords =
   37.19 -    Keyword.Keywords.empty +
   37.20 -      "%" + "(" + ")" + "," + "::" + "==" + AND + BEGIN + IMPORTS + KEYWORDS +
   37.21 -      (HEADER, Keyword.HEADING) +
   37.22 -      (CHAPTER, Keyword.HEADING) +
   37.23 -      (SECTION, Keyword.HEADING) +
   37.24 -      (SUBSECTION, Keyword.HEADING) +
   37.25 -      (SUBSUBSECTION, Keyword.HEADING) +
   37.26 -      (THEORY, Keyword.THY_BEGIN)
   37.27 +  private val bootstrap_header: Keywords =
   37.28 +    List(
   37.29 +      ("%", None, None),
   37.30 +      ("(", None, None),
   37.31 +      (")", None, None),
   37.32 +      (",", None, None),
   37.33 +      ("::", None, None),
   37.34 +      ("==", None, None),
   37.35 +      (AND, None, None),
   37.36 +      (BEGIN, None, None),
   37.37 +      (IMPORTS, None, None),
   37.38 +      (KEYWORDS, None, None),
   37.39 +      (HEADER, Some(((Keyword.HEADING, Nil), Nil)), None),
   37.40 +      (CHAPTER, Some(((Keyword.HEADING, Nil), Nil)), None),
   37.41 +      (SECTION, Some(((Keyword.HEADING, Nil), Nil)), None),
   37.42 +      (SUBSECTION, Some(((Keyword.HEADING, Nil), Nil)), None),
   37.43 +      (SUBSUBSECTION, Some(((Keyword.HEADING, Nil), Nil)), None),
   37.44 +      (THEORY, Some((Keyword.THY_BEGIN, Nil), List("theory")), None),
   37.45 +      ("ML_file", Some((Keyword.THY_LOAD, Nil), List("ML")), None))
   37.46 +
   37.47 +  private val bootstrap_keywords =
   37.48 +    Keyword.Keywords.empty.add_keywords(bootstrap_header)
   37.49 +
   37.50 +  def bootstrap_syntax(): Outer_Syntax =
   37.51 +    Outer_Syntax.init().add_keywords(bootstrap_header)
   37.52  
   37.53  
   37.54    /* theory file name */
   37.55 @@ -101,7 +121,7 @@
   37.56  
   37.57    def read(reader: Reader[Char]): Thy_Header =
   37.58    {
   37.59 -    val token = Token.Parsers.token(header_keywords)
   37.60 +    val token = Token.Parsers.token(bootstrap_keywords)
   37.61      val toks = new mutable.ListBuffer[Token]
   37.62  
   37.63      @tailrec def scan_to_begin(in: Reader[Char])
   37.64 @@ -123,11 +143,6 @@
   37.65  
   37.66    def read(source: CharSequence): Thy_Header =
   37.67      read(new CharSequenceReader(source))
   37.68 -
   37.69 -
   37.70 -  /* keywords */
   37.71 -
   37.72 -  type Keywords = List[(String, Option[Keyword.Spec], Option[String])]
   37.73  }
   37.74  
   37.75  
    38.1 --- a/src/Pure/Thy/thy_info.ML	Fri Nov 07 16:22:25 2014 +0100
    38.2 +++ b/src/Pure/Thy/thy_info.ML	Fri Nov 07 16:36:55 2014 +0100
    38.3 @@ -373,7 +373,7 @@
    38.4  fun script_thy pos txt thy =
    38.5    let
    38.6      val trs =
    38.7 -      Outer_Syntax.parse (Outer_Syntax.get_syntax ()) pos txt
    38.8 +      Outer_Syntax.parse thy pos txt
    38.9        |> map (Toplevel.modify_init (K thy));
   38.10      val end_pos = if null trs then pos else Toplevel.pos_of (List.last trs);
   38.11      val end_state = fold (Toplevel.command_exception true) trs Toplevel.toplevel;
    39.1 --- a/src/Pure/Thy/thy_output.ML	Fri Nov 07 16:22:25 2014 +0100
    39.2 +++ b/src/Pure/Thy/thy_output.ML	Fri Nov 07 16:36:55 2014 +0100
    39.3 @@ -22,11 +22,9 @@
    39.4        theory -> theory
    39.5    val boolean: string -> bool
    39.6    val integer: string -> int
    39.7 -  datatype markup = Markup | MarkupEnv | Verbatim
    39.8 -  val eval_antiq: Keyword.keywords -> Toplevel.state -> Antiquote.antiq -> string
    39.9 +  val eval_antiq: Toplevel.state -> Antiquote.antiq -> string
   39.10    val check_text: Symbol_Pos.source -> Toplevel.state -> unit
   39.11 -  val present_thy: Keyword.keywords -> (markup -> string -> bool) ->
   39.12 -    (Toplevel.transition * Toplevel.state) list -> Token.T list -> Buffer.T
   39.13 +  val present_thy: theory -> (Toplevel.transition * Toplevel.state) list -> Token.T list -> Buffer.T
   39.14    val pretty_text: Proof.context -> string -> Pretty.T
   39.15    val pretty_term: Proof.context -> term -> Pretty.T
   39.16    val pretty_thm: Proof.context -> thm -> Pretty.T
   39.17 @@ -35,6 +33,12 @@
   39.18      Token.src -> 'a list -> Pretty.T list
   39.19    val output: Proof.context -> Pretty.T list -> string
   39.20    val verbatim_text: Proof.context -> string -> string
   39.21 +  val local_theory_markup: (xstring * Position.T) option * Symbol_Pos.source ->
   39.22 +    Toplevel.transition -> Toplevel.transition
   39.23 +  val proof_markup: Symbol_Pos.source -> Toplevel.transition -> Toplevel.transition
   39.24 +  val header_markup: Symbol_Pos.source -> Toplevel.transition -> Toplevel.transition
   39.25 +  val heading_markup: (xstring * Position.T) option * Symbol_Pos.source ->
   39.26 +    Toplevel.transition -> Toplevel.transition
   39.27  end;
   39.28  
   39.29  structure Thy_Output: THY_OUTPUT =
   39.30 @@ -158,10 +162,18 @@
   39.31  
   39.32  (* eval_antiq *)
   39.33  
   39.34 -fun eval_antiq keywords state ((ss, {range = (pos, _), ...}): Antiquote.antiq) =
   39.35 +fun eval_antiq state ((ss, {range = (pos, _), ...}): Antiquote.antiq) =
   39.36    let
   39.37 +    val keywords =
   39.38 +      (case try Toplevel.presentation_context_of state of
   39.39 +        SOME ctxt => Thy_Header.get_keywords' ctxt
   39.40 +      | NONE =>
   39.41 +          error ("Unknown context -- cannot expand document antiquotations" ^
   39.42 +            Position.here pos));
   39.43 +
   39.44      val (opts, src) = Token.read_antiq keywords antiq (ss, pos);
   39.45      fun cmd ctxt = wrap ctxt (fn () => command src state ctxt) ();
   39.46 +
   39.47      val preview_ctxt = fold option opts (Toplevel.presentation_context_of state);
   39.48      val print_ctxt = Context_Position.set_visible false preview_ctxt;
   39.49      val _ = cmd preview_ctxt;
   39.50 @@ -171,26 +183,22 @@
   39.51  
   39.52  (* check_text *)
   39.53  
   39.54 -fun eval_antiquote keywords state (txt, pos) =
   39.55 +fun eval_antiquote state (txt, pos) =
   39.56    let
   39.57      fun words (Antiquote.Text ss) = [(#1 (Symbol_Pos.range ss), Markup.words)]
   39.58        | words (Antiquote.Antiq _) = [];
   39.59  
   39.60      fun expand (Antiquote.Text ss) = Symbol_Pos.content ss
   39.61 -      | expand (Antiquote.Antiq antiq) = eval_antiq keywords state antiq;
   39.62 +      | expand (Antiquote.Antiq antiq) = eval_antiq state antiq;
   39.63  
   39.64      val ants = Antiquote.read (Symbol_Pos.explode (txt, pos), pos);
   39.65      val _ = Position.reports (maps words ants);
   39.66 -  in
   39.67 -    if Toplevel.is_toplevel state andalso not (forall Antiquote.is_text ants) then
   39.68 -      error ("Unknown context -- cannot expand document antiquotations" ^ Position.here pos)
   39.69 -    else implode (map expand ants)
   39.70 -  end;
   39.71 +  in implode (map expand ants) end;
   39.72  
   39.73  fun check_text {delimited, text, pos} state =
   39.74   (Position.report pos (Markup.language_document delimited);
   39.75    if Toplevel.is_skipped_proof state then ()
   39.76 -  else ignore (eval_antiquote (Keyword.get_keywords ()) state (text, pos)));
   39.77 +  else ignore (eval_antiquote state (text, pos)));
   39.78  
   39.79  
   39.80  
   39.81 @@ -207,8 +215,8 @@
   39.82    | MarkupEnvToken of string * (string * Position.T)
   39.83    | VerbatimToken of string * Position.T;
   39.84  
   39.85 -fun output_token keywords state =
   39.86 -  let val eval = eval_antiquote keywords state in
   39.87 +fun output_token state =
   39.88 +  let val eval = eval_antiquote state in
   39.89      fn NoToken => ""
   39.90       | BasicToken tok => Latex.output_basic tok
   39.91       | MarkupToken (cmd, txt) => Latex.output_markup cmd (eval txt)
   39.92 @@ -268,7 +276,7 @@
   39.93  fun present_span keywords span state state' (tag_stack, active_tag, newline, buffer, present_cont) =
   39.94    let
   39.95      val present = fold (fn (tok, (flag, 0)) =>
   39.96 -        Buffer.add (output_token keywords state' tok)
   39.97 +        Buffer.add (output_token state' tok)
   39.98          #> Buffer.add flag
   39.99        | _ => I);
  39.100  
  39.101 @@ -321,8 +329,6 @@
  39.102  
  39.103  (* present_thy *)
  39.104  
  39.105 -datatype markup = Markup | MarkupEnv | Verbatim;
  39.106 -
  39.107  local
  39.108  
  39.109  val space_proper =
  39.110 @@ -350,8 +356,12 @@
  39.111  
  39.112  in
  39.113  
  39.114 -fun present_thy keywords is_markup command_results toks =
  39.115 +fun present_thy thy command_results toks =
  39.116    let
  39.117 +    val keywords = Thy_Header.get_keywords thy;
  39.118 +    val is_markup = Outer_Syntax.is_markup thy;
  39.119 +
  39.120 +
  39.121      (* tokens *)
  39.122  
  39.123      val ignored = Scan.state --| ignore
  39.124 @@ -382,9 +392,9 @@
  39.125  
  39.126      val token =
  39.127        ignored ||
  39.128 -      markup Markup MarkupToken Latex.markup_true ||
  39.129 -      markup MarkupEnv MarkupEnvToken Latex.markup_true ||
  39.130 -      markup Verbatim (VerbatimToken o #2) "" ||
  39.131 +      markup Outer_Syntax.Markup MarkupToken Latex.markup_true ||
  39.132 +      markup Outer_Syntax.Markup_Env MarkupEnvToken Latex.markup_true ||
  39.133 +      markup Outer_Syntax.Verbatim (VerbatimToken o #2) "" ||
  39.134        command || cmt || other;
  39.135  
  39.136  
  39.137 @@ -690,4 +700,29 @@
  39.138        (Context_Position.reports ctxt [(pos, Markup.language_path), (pos, Markup.url name)];
  39.139         enclose "\\url{" "}" name)));
  39.140  
  39.141 +
  39.142 +
  39.143 +(** markup commands **)
  39.144 +
  39.145 +fun local_theory_markup (loc, txt) = Toplevel.present_local_theory loc (check_text txt);
  39.146 +val proof_markup = Toplevel.present_proof o check_text;
  39.147 +
  39.148 +fun reject_target NONE = ()
  39.149 +  | reject_target (SOME (_, pos)) =
  39.150 +      error ("Illegal target specification -- not a theory context" ^ Position.here pos);
  39.151 +
  39.152 +fun header_markup txt =
  39.153 +  Toplevel.keep (fn state =>
  39.154 +    if Toplevel.is_toplevel state then
  39.155 +     (legacy_feature "Obsolete 'header' command -- use 'chapter', 'section' etc. instead";
  39.156 +      check_text txt state)
  39.157 +    else raise Toplevel.UNDEF);
  39.158 +
  39.159 +fun heading_markup (loc, txt) =
  39.160 +  Toplevel.keep (fn state =>
  39.161 +    if Toplevel.is_toplevel state then (reject_target loc; check_text txt state)
  39.162 +    else raise Toplevel.UNDEF) o
  39.163 +  local_theory_markup (loc, txt) o
  39.164 +  Toplevel.present_proof (fn state => (reject_target loc; check_text txt state));
  39.165 +
  39.166  end;
    40.1 --- a/src/Pure/Tools/build.ML	Fri Nov 07 16:22:25 2014 +0100
    40.2 +++ b/src/Pure/Tools/build.ML	Fri Nov 07 16:36:55 2014 +0100
    40.3 @@ -157,7 +157,6 @@
    40.4          theories |>
    40.5            (List.app (use_theories_condition last_timing)
    40.6              |> session_timing name verbose
    40.7 -            |> Unsynchronized.setmp Outer_Syntax.batch_mode true
    40.8              |> Unsynchronized.setmp Output.protocol_message_fn protocol_message
    40.9              |> Multithreading.max_threads_setmp (Options.int options "threads")
   40.10              |> Exn.capture);
    41.1 --- a/src/Pure/Tools/build.scala	Fri Nov 07 16:22:25 2014 +0100
    41.2 +++ b/src/Pure/Tools/build.scala	Fri Nov 07 16:36:55 2014 +0100
    41.3 @@ -437,7 +437,8 @@
    41.4              val (loaded_theories0, known_theories0, syntax0) =
    41.5                info.parent.map(deps(_)) match {
    41.6                  case None =>
    41.7 -                  (Set.empty[String], Map.empty[String, Document.Node.Name], Pure_Syn.init())
    41.8 +                  (Set.empty[String], Map.empty[String, Document.Node.Name],
    41.9 +                    Thy_Header.bootstrap_syntax())
   41.10                  case Some(parent) =>
   41.11                    (parent.loaded_theories, parent.known_theories, parent.syntax)
   41.12                }
    42.1 --- a/src/Pure/Tools/find_consts.ML	Fri Nov 07 16:22:25 2014 +0100
    42.2 +++ b/src/Pure/Tools/find_consts.ML	Fri Nov 07 16:36:55 2014 +0100
    42.3 @@ -140,7 +140,7 @@
    42.4  
    42.5  val query = Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion);
    42.6  
    42.7 -val query_keywords = Keyword.add_keywords (":", NONE) Keyword.empty_keywords;
    42.8 +val query_keywords = Keyword.add_keywords [(":", NONE)] Keyword.empty_keywords;
    42.9  
   42.10  in
   42.11  
    43.1 --- a/src/Pure/Tools/find_theorems.ML	Fri Nov 07 16:22:25 2014 +0100
    43.2 +++ b/src/Pure/Tools/find_theorems.ML	Fri Nov 07 16:36:55 2014 +0100
    43.3 @@ -526,7 +526,7 @@
    43.4  
    43.5  val query = Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion);
    43.6  
    43.7 -val query_keywords = Keyword.add_keywords (":", NONE) Keyword.empty_keywords;
    43.8 +val query_keywords = Keyword.add_keywords [(":", NONE)] Keyword.empty_keywords;
    43.9  
   43.10  in
   43.11  
    44.1 --- a/src/Pure/Tools/rail.ML	Fri Nov 07 16:22:25 2014 +0100
    44.2 +++ b/src/Pure/Tools/rail.ML	Fri Nov 07 16:36:55 2014 +0100
    44.3 @@ -316,7 +316,7 @@
    44.4  
    44.5  fun output_rules state rules =
    44.6    let
    44.7 -    val output_antiq = Thy_Output.eval_antiq (Keyword.get_keywords ()) state;
    44.8 +    val output_antiq = Thy_Output.eval_antiq state;
    44.9      fun output_text b s =
   44.10        Output.output s
   44.11        |> b ? enclose "\\isakeyword{" "}"
    45.1 --- a/src/Pure/build-jars	Fri Nov 07 16:22:25 2014 +0100
    45.2 +++ b/src/Pure/build-jars	Fri Nov 07 16:36:55 2014 +0100
    45.3 @@ -99,7 +99,6 @@
    45.4    Tools/update_header.scala
    45.5    Tools/update_semicolons.scala
    45.6    library.scala
    45.7 -  pure_syn.scala
    45.8    term.scala
    45.9    term_xml.scala
   45.10    "../Tools/Graphview/src/graph_panel.scala"
    46.1 --- a/src/Pure/pure_syn.ML	Fri Nov 07 16:22:25 2014 +0100
    46.2 +++ b/src/Pure/pure_syn.ML	Fri Nov 07 16:36:55 2014 +0100
    46.3 @@ -1,50 +1,36 @@
    46.4  (*  Title:      Pure/pure_syn.ML
    46.5      Author:     Makarius
    46.6  
    46.7 -Minimal outer syntax for bootstrapping Isabelle/Pure.
    46.8 +Outer syntax for bootstrapping Isabelle/Pure.
    46.9  *)
   46.10  
   46.11  structure Pure_Syn: sig end =
   46.12  struct
   46.13  
   46.14 -(* keywords *)
   46.15 -
   46.16 -val keywords: Thy_Header.keywords =
   46.17 - [("theory", SOME (("thy_begin", []), ["theory"])),
   46.18 -  ("ML_file", SOME (("thy_load", []), ["ML"]))];
   46.19 +val _ =
   46.20 +  Outer_Syntax.markup_command Outer_Syntax.Markup ("header", @{here}) "theory header"
   46.21 +    (Parse.document_source >> Thy_Output.header_markup);
   46.22  
   46.23 -fun command_spec (name, pos) =
   46.24 -  (case AList.lookup (op =) keywords name of
   46.25 -    SOME (SOME spec) => Keyword.command_spec ((name, spec), pos)
   46.26 -  | _ => error ("Bad command specification " ^ quote name ^ Position.here pos));
   46.27 -
   46.28 -val _ = Thy_Header.define_keywords keywords;
   46.29 -val _ = Theory.setup (fold Thy_Header.declare_keyword keywords);
   46.30 -
   46.31 -
   46.32 -(* commands *)
   46.33 +val _ =
   46.34 +  Outer_Syntax.markup_command Outer_Syntax.Markup ("chapter", @{here}) "chapter heading"
   46.35 +    (Parse.opt_target -- Parse.document_source >> Thy_Output.heading_markup);
   46.36  
   46.37  val _ =
   46.38 -  Outer_Syntax.command
   46.39 -    (command_spec ("theory", @{here})) "begin theory"
   46.40 +  Outer_Syntax.markup_command Outer_Syntax.Markup ("section", @{here}) "section heading"
   46.41 +    (Parse.opt_target -- Parse.document_source >> Thy_Output.heading_markup);
   46.42 +
   46.43 +val _ =
   46.44 +  Outer_Syntax.markup_command Outer_Syntax.Markup ("subsection", @{here}) "subsection heading"
   46.45 +    (Parse.opt_target -- Parse.document_source >> Thy_Output.heading_markup);
   46.46 +
   46.47 +val _ =
   46.48 +  Outer_Syntax.markup_command Outer_Syntax.Markup ("subsubsection", @{here}) "subsubsection heading"
   46.49 +    (Parse.opt_target -- Parse.document_source >> Thy_Output.heading_markup);
   46.50 +
   46.51 +val _ =
   46.52 +  Outer_Syntax.command ("theory", @{here}) "begin theory"
   46.53      (Thy_Header.args >>
   46.54        (fn _ => Toplevel.init_theory (fn () => error "Missing theory initialization")));
   46.55  
   46.56 -val _ =
   46.57 -  Outer_Syntax.command
   46.58 -    (command_spec ("ML_file", @{here})) "ML text from file"
   46.59 -    (Resources.parse_files "ML_file" >> (fn files => Toplevel.generic_theory (fn gthy =>
   46.60 -        let
   46.61 -          val [{src_path, lines, digest, pos}] = files (Context.theory_of gthy);
   46.62 -          val provide = Resources.provide (src_path, digest);
   46.63 -          val source = {delimited = true, text = cat_lines lines, pos = pos};
   46.64 -          val flags = {SML = false, exchange = false, redirect = true, verbose = true};
   46.65 -        in
   46.66 -          gthy
   46.67 -          |> ML_Context.exec (fn () => ML_Context.eval_source flags source)
   46.68 -          |> Local_Theory.propagate_ml_env
   46.69 -          |> Context.mapping provide (Local_Theory.background_theory provide)
   46.70 -        end)));
   46.71 -
   46.72  end;
   46.73  
    47.1 --- a/src/Pure/pure_syn.scala	Fri Nov 07 16:22:25 2014 +0100
    47.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    47.3 @@ -1,19 +0,0 @@
    47.4 -/*  Title:      Pure/pure_syn.scala
    47.5 -    Author:     Makarius
    47.6 -
    47.7 -Minimal outer syntax for bootstrapping Isabelle/Pure.
    47.8 -*/
    47.9 -
   47.10 -package isabelle
   47.11 -
   47.12 -
   47.13 -object Pure_Syn
   47.14 -{
   47.15 -  private val keywords: Thy_Header.Keywords =
   47.16 -    List(
   47.17 -      ("theory", Some((("thy_begin", Nil), List("theory"))), None),
   47.18 -      ("ML_file", Some((("thy_load", Nil), List("ML"))), None))
   47.19 -
   47.20 -  def init(): Outer_Syntax = Outer_Syntax.init().add_keywords(keywords)
   47.21 -}
   47.22 -
    48.1 --- a/src/Tools/Code/code_target.ML	Fri Nov 07 16:22:25 2014 +0100
    48.2 +++ b/src/Tools/Code/code_target.ML	Fri Nov 07 16:36:55 2014 +0100
    48.3 @@ -693,9 +693,10 @@
    48.4  
    48.5  fun codegen_tool thyname cmd_expr =
    48.6    let
    48.7 -    val ctxt = Proof_Context.init_global (Thy_Info.get_theory thyname);
    48.8 +    val thy = Thy_Info.get_theory thyname;
    48.9 +    val ctxt = Proof_Context.init_global thy;
   48.10      val parse = Scan.read Token.stopper (Parse.!!! code_exprP) o
   48.11 -      (filter Token.is_proper o Outer_Syntax.scan (Keyword.get_keywords ()) Position.none);
   48.12 +      (filter Token.is_proper o Outer_Syntax.scan (Thy_Header.get_keywords thy) Position.none);
   48.13    in case parse cmd_expr
   48.14     of SOME f => (writeln "Now generating code..."; f ctxt)
   48.15      | NONE => error ("Bad directive " ^ quote cmd_expr)
    49.1 --- a/src/Tools/jEdit/src/plugin.scala	Fri Nov 07 16:22:25 2014 +0100
    49.2 +++ b/src/Tools/jEdit/src/plugin.scala	Fri Nov 07 16:36:55 2014 +0100
    49.3 @@ -261,7 +261,7 @@
    49.4          }
    49.5  
    49.6        case Session.Ready =>
    49.7 -        PIDE.session.update_options(PIDE.options.value)
    49.8 +        PIDE.session.init_options(PIDE.options.value)
    49.9          PIDE.init_models()
   49.10  
   49.11          if (!Isabelle.continuous_checking) {