# HG changeset patch # User wenzelm # Date 1331899530 -3600 # Node ID 0ec8f04e753ad003d977ea6c7e220c2c33966132 # Parent 0c15caf47040b1bd29823cb155e811c0e72e8d45 define keywords early when processing the theory header, before running the body commands; diff -r 0c15caf47040 -r 0ec8f04e753a src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Fri Mar 16 11:26:55 2012 +0100 +++ b/src/Pure/Isar/isar_syn.ML Fri Mar 16 13:05:30 2012 +0100 @@ -9,11 +9,8 @@ (** keywords **) -(*keep keywords consistent with the parsers, otherwise be prepared for - unexpected errors*) - val _ = Context.>> (Context.map_theory - (fold (fn name => Thy_Header.declare_keyword (name, NONE)) + (fold (fn name => (Keyword.define (name, NONE); Thy_Header.declare_keyword (name, NONE))) ["!!", "!", "%", "(", ")", "+", ",", "--", ":", "::", ";", "<", "<=", "=", "==", "=>", "?", "[", "\\", "\\", "\\", "\\", "\\", "]", diff -r 0c15caf47040 -r 0ec8f04e753a src/Pure/Isar/keyword.ML --- a/src/Pure/Isar/keyword.ML Fri Mar 16 11:26:55 2012 +0100 +++ b/src/Pure/Isar/keyword.ML Fri Mar 16 13:05:30 2012 +0100 @@ -45,7 +45,7 @@ val dest: unit -> string list * string list val keyword_statusN: string val status: unit -> unit - val declare: string -> T option -> unit + val define: string * T option -> unit val is_diag: string -> bool val is_control: string -> bool val is_regular: string -> bool @@ -214,15 +214,15 @@ in () end; -(* declare *) +(* define *) -fun declare name NONE = +fun define (name, NONE) = (change_keywords (fn ((minor, major), commands) => let val minor' = Scan.extend_lexicon (Symbol.explode name) minor; in ((minor', major), commands) end); keyword_status name) - | declare name (SOME kind) = + | define (name, SOME kind) = (change_keywords (fn ((minor, major), commands) => let val major' = Scan.extend_lexicon (Symbol.explode name) major; diff -r 0c15caf47040 -r 0ec8f04e753a src/Pure/Isar/outer_syntax.ML --- a/src/Pure/Isar/outer_syntax.ML Fri Mar 16 11:26:55 2012 +0100 +++ b/src/Pure/Isar/outer_syntax.ML Fri Mar 16 13:05:30 2012 +0100 @@ -131,7 +131,7 @@ if k = SOME kind then () else error ("Inconsistent outer syntax keyword declaration " ^ quote name) | NONE => - if Context.theory_name thy = Context.PureN then Keyword.declare name (SOME kind) + if Context.theory_name thy = Context.PureN then Keyword.define (name, SOME kind) else error ("Undeclared outer syntax command " ^ quote name)); in Unsynchronized.change global_outer_syntax (map_commands (fn commands => diff -r 0c15caf47040 -r 0ec8f04e753a src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Fri Mar 16 11:26:55 2012 +0100 +++ b/src/Pure/PIDE/document.ML Fri Mar 16 13:05:30 2012 +0100 @@ -213,10 +213,8 @@ | Header header => let val imports = (case header of Exn.Res (_, {imports, ...}) => imports | _ => []); - val keywords = (case header of Exn.Res (_, {keywords, ...}) => keywords | _ => []); val header' = - (List.app (fn (name, decl) => - Keyword.declare name (Option.map Keyword.make decl)) keywords; header) + ((case header of Exn.Res (_, h) => Thy_Header.define_keywords h | _ => ()); header) handle exn as ERROR _ => Exn.Exn exn; val nodes1 = nodes |> default_node name diff -r 0c15caf47040 -r 0ec8f04e753a src/Pure/Thy/thy_header.ML --- a/src/Pure/Thy/thy_header.ML Fri Mar 16 11:26:55 2012 +0100 +++ b/src/Pure/Thy/thy_header.ML Fri Mar 16 13:05:30 2012 +0100 @@ -12,6 +12,7 @@ uses: (Path.T * bool) list} val make: string -> string list -> (string * (string * string list) option) list -> (Path.T * bool) list -> header + val define_keywords: header -> unit val declare_keyword: string * (string * string list) option -> theory -> theory val the_keyword: theory -> string -> Keyword.T option val args: header parser @@ -33,6 +34,9 @@ (** keyword declarations **) +fun define_keywords ({keywords, ...}: header) = + List.app (fn (name, decl) => Keyword.define (name, Option.map Keyword.make decl)) keywords; + fun err_dup name = error ("Inconsistent declaration of outer syntax keyword " ^ quote name); structure Data = Theory_Data @@ -44,9 +48,7 @@ ); fun declare_keyword (name, decl) = Data.map (fn data => - let - val kind = Option.map Keyword.make decl; - val _ = Keyword.declare name kind; + let val kind = Option.map Keyword.make decl in Symtab.update_new (name, kind) data handle Symtab.DUP name => err_dup name end); fun the_keyword thy name = diff -r 0c15caf47040 -r 0ec8f04e753a src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Fri Mar 16 11:26:55 2012 +0100 +++ b/src/Pure/Thy/thy_info.ML Fri Mar 16 13:05:30 2012 +0100 @@ -314,6 +314,7 @@ val {name, imports, ...} = header; val _ = kill_thy name; val _ = use_thys_wrt dir imports; + val _ = Thy_Header.define_keywords header; val parents = map (get_theory o base_name) imports; in Thy_Load.begin_theory dir header parents end; diff -r 0c15caf47040 -r 0ec8f04e753a src/Pure/Thy/thy_load.ML --- a/src/Pure/Thy/thy_load.ML Fri Mar 16 11:26:55 2012 +0100 +++ b/src/Pure/Thy/thy_load.ML Fri Mar 16 13:05:30 2012 +0100 @@ -170,15 +170,17 @@ fun load_thy update_time dir header pos text parents = let - val (lexs, outer_syntax) = Outer_Syntax.get_syntax (); val time = ! Toplevel.timing; val {name, imports, uses, ...} = header; + val _ = Thy_Header.define_keywords header; val _ = Present.init_theory name; fun init () = begin_theory dir header parents |> Present.begin_theory update_time dir uses; + val (lexs, outer_syntax) = Outer_Syntax.get_syntax (); + val toks = Thy_Syntax.parse_tokens lexs pos text; val spans = Thy_Syntax.parse_spans toks; val elements = diff -r 0c15caf47040 -r 0ec8f04e753a src/Pure/Thy/thy_output.ML --- a/src/Pure/Thy/thy_output.ML Fri Mar 16 11:26:55 2012 +0100 +++ b/src/Pure/Thy/thy_output.ML Fri Mar 16 13:05:30 2012 +0100 @@ -626,7 +626,7 @@ (* embedded lemma *) -val _ = Keyword.declare "by" NONE; (*overlap with command category*) +val _ = Keyword.define ("by", NONE); (*overlap with command category*) val _ = Context.>> (Context.map_theory