define keywords early when processing the theory header, before running the body commands;
authorwenzelm
Fri Mar 16 13:05:30 2012 +0100 (2012-03-16)
changeset 469580ec8f04e753a
parent 46957 0c15caf47040
child 46959 cdc791910460
define keywords early when processing the theory header, before running the body commands;
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/keyword.ML
src/Pure/Isar/outer_syntax.ML
src/Pure/PIDE/document.ML
src/Pure/Thy/thy_header.ML
src/Pure/Thy/thy_info.ML
src/Pure/Thy/thy_load.ML
src/Pure/Thy/thy_output.ML
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Fri Mar 16 11:26:55 2012 +0100
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Fri Mar 16 13:05:30 2012 +0100
     1.3 @@ -9,11 +9,8 @@
     1.4  
     1.5  (** keywords **)
     1.6  
     1.7 -(*keep keywords consistent with the parsers, otherwise be prepared for
     1.8 -  unexpected errors*)
     1.9 -
    1.10  val _ = Context.>> (Context.map_theory
    1.11 -  (fold (fn name => Thy_Header.declare_keyword (name, NONE))
    1.12 +  (fold (fn name => (Keyword.define (name, NONE); Thy_Header.declare_keyword (name, NONE)))
    1.13     ["!!", "!", "%", "(", ")", "+", ",", "--", ":", "::", ";", "<", "<=",
    1.14      "=", "==", "=>", "?", "[", "\\<equiv>", "\\<leftharpoondown>",
    1.15      "\\<rightharpoonup>", "\\<rightleftharpoons>", "\\<subseteq>", "]",
     2.1 --- a/src/Pure/Isar/keyword.ML	Fri Mar 16 11:26:55 2012 +0100
     2.2 +++ b/src/Pure/Isar/keyword.ML	Fri Mar 16 13:05:30 2012 +0100
     2.3 @@ -45,7 +45,7 @@
     2.4    val dest: unit -> string list * string list
     2.5    val keyword_statusN: string
     2.6    val status: unit -> unit
     2.7 -  val declare: string -> T option -> unit
     2.8 +  val define: string * T option -> unit
     2.9    val is_diag: string -> bool
    2.10    val is_control: string -> bool
    2.11    val is_regular: string -> bool
    2.12 @@ -214,15 +214,15 @@
    2.13    in () end;
    2.14  
    2.15  
    2.16 -(* declare *)
    2.17 +(* define *)
    2.18  
    2.19 -fun declare name NONE =
    2.20 +fun define (name, NONE) =
    2.21       (change_keywords (fn ((minor, major), commands) =>
    2.22          let
    2.23            val minor' = Scan.extend_lexicon (Symbol.explode name) minor;
    2.24          in ((minor', major), commands) end);
    2.25        keyword_status name)
    2.26 -  | declare name (SOME kind) =
    2.27 +  | define (name, SOME kind) =
    2.28       (change_keywords (fn ((minor, major), commands) =>
    2.29          let
    2.30            val major' = Scan.extend_lexicon (Symbol.explode name) major;
     3.1 --- a/src/Pure/Isar/outer_syntax.ML	Fri Mar 16 11:26:55 2012 +0100
     3.2 +++ b/src/Pure/Isar/outer_syntax.ML	Fri Mar 16 13:05:30 2012 +0100
     3.3 @@ -131,7 +131,7 @@
     3.4            if k = SOME kind then ()
     3.5            else error ("Inconsistent outer syntax keyword declaration " ^ quote name)
     3.6        | NONE =>
     3.7 -          if Context.theory_name thy = Context.PureN then Keyword.declare name (SOME kind)
     3.8 +          if Context.theory_name thy = Context.PureN then Keyword.define (name, SOME kind)
     3.9            else error ("Undeclared outer syntax command " ^ quote name));
    3.10    in
    3.11      Unsynchronized.change global_outer_syntax (map_commands (fn commands =>
     4.1 --- a/src/Pure/PIDE/document.ML	Fri Mar 16 11:26:55 2012 +0100
     4.2 +++ b/src/Pure/PIDE/document.ML	Fri Mar 16 13:05:30 2012 +0100
     4.3 @@ -213,10 +213,8 @@
     4.4      | Header header =>
     4.5          let
     4.6            val imports = (case header of Exn.Res (_, {imports, ...}) => imports | _ => []);
     4.7 -          val keywords = (case header of Exn.Res (_, {keywords, ...}) => keywords | _ => []);
     4.8            val header' =
     4.9 -            (List.app (fn (name, decl) =>
    4.10 -                Keyword.declare name (Option.map Keyword.make decl)) keywords; header)
    4.11 +            ((case header of Exn.Res (_, h) => Thy_Header.define_keywords h | _ => ()); header)
    4.12                handle exn as ERROR _ => Exn.Exn exn;
    4.13            val nodes1 = nodes
    4.14              |> default_node name
     5.1 --- a/src/Pure/Thy/thy_header.ML	Fri Mar 16 11:26:55 2012 +0100
     5.2 +++ b/src/Pure/Thy/thy_header.ML	Fri Mar 16 13:05:30 2012 +0100
     5.3 @@ -12,6 +12,7 @@
     5.4      uses: (Path.T * bool) list}
     5.5    val make: string -> string list -> (string * (string * string list) option) list ->
     5.6      (Path.T * bool) list -> header
     5.7 +  val define_keywords: header -> unit
     5.8    val declare_keyword: string * (string * string list) option -> theory -> theory
     5.9    val the_keyword: theory -> string -> Keyword.T option
    5.10    val args: header parser
    5.11 @@ -33,6 +34,9 @@
    5.12  
    5.13  (** keyword declarations **)
    5.14  
    5.15 +fun define_keywords ({keywords, ...}: header) =
    5.16 +  List.app (fn (name, decl) => Keyword.define (name, Option.map Keyword.make decl)) keywords;
    5.17 +
    5.18  fun err_dup name = error ("Inconsistent declaration of outer syntax keyword " ^ quote name);
    5.19  
    5.20  structure Data = Theory_Data
    5.21 @@ -44,9 +48,7 @@
    5.22  );
    5.23  
    5.24  fun declare_keyword (name, decl) = Data.map (fn data =>
    5.25 -  let
    5.26 -    val kind = Option.map Keyword.make decl;
    5.27 -    val _ = Keyword.declare name kind;
    5.28 +  let val kind = Option.map Keyword.make decl
    5.29    in Symtab.update_new (name, kind) data handle Symtab.DUP name => err_dup name end);
    5.30  
    5.31  fun the_keyword thy name =
     6.1 --- a/src/Pure/Thy/thy_info.ML	Fri Mar 16 11:26:55 2012 +0100
     6.2 +++ b/src/Pure/Thy/thy_info.ML	Fri Mar 16 13:05:30 2012 +0100
     6.3 @@ -314,6 +314,7 @@
     6.4      val {name, imports, ...} = header;
     6.5      val _ = kill_thy name;
     6.6      val _ = use_thys_wrt dir imports;
     6.7 +    val _ = Thy_Header.define_keywords header;
     6.8      val parents = map (get_theory o base_name) imports;
     6.9    in Thy_Load.begin_theory dir header parents end;
    6.10  
     7.1 --- a/src/Pure/Thy/thy_load.ML	Fri Mar 16 11:26:55 2012 +0100
     7.2 +++ b/src/Pure/Thy/thy_load.ML	Fri Mar 16 13:05:30 2012 +0100
     7.3 @@ -170,15 +170,17 @@
     7.4  
     7.5  fun load_thy update_time dir header pos text parents =
     7.6    let
     7.7 -    val (lexs, outer_syntax) = Outer_Syntax.get_syntax ();
     7.8      val time = ! Toplevel.timing;
     7.9  
    7.10      val {name, imports, uses, ...} = header;
    7.11 +    val _ = Thy_Header.define_keywords header;
    7.12      val _ = Present.init_theory name;
    7.13      fun init () =
    7.14        begin_theory dir header parents
    7.15        |> Present.begin_theory update_time dir uses;
    7.16  
    7.17 +    val (lexs, outer_syntax) = Outer_Syntax.get_syntax ();
    7.18 +
    7.19      val toks = Thy_Syntax.parse_tokens lexs pos text;
    7.20      val spans = Thy_Syntax.parse_spans toks;
    7.21      val elements =
     8.1 --- a/src/Pure/Thy/thy_output.ML	Fri Mar 16 11:26:55 2012 +0100
     8.2 +++ b/src/Pure/Thy/thy_output.ML	Fri Mar 16 13:05:30 2012 +0100
     8.3 @@ -626,7 +626,7 @@
     8.4  
     8.5  (* embedded lemma *)
     8.6  
     8.7 -val _ = Keyword.declare "by" NONE;  (*overlap with command category*)
     8.8 +val _ = Keyword.define ("by", NONE);  (*overlap with command category*)
     8.9  
    8.10  val _ =
    8.11    Context.>> (Context.map_theory