# HG changeset patch # User wenzelm # Date 1303570932 -7200 # Node ID bbce02fcba60866c5a6598eea0d046a2c7c68a4b # Parent 1ba52683512a414a99219d3ffe3e4c2f339d98c3 added Name_Space.check/get convenience; diff -r 1ba52683512a -r bbce02fcba60 src/Pure/General/name_space.ML --- a/src/Pure/General/name_space.ML Sat Apr 23 16:30:00 2011 +0200 +++ b/src/Pure/General/name_space.ML Sat Apr 23 17:02:12 2011 +0200 @@ -49,6 +49,8 @@ val declare: Proof.context -> bool -> naming -> binding -> T -> string * T val alias: naming -> binding -> string -> T -> T type 'a table = T * 'a Symtab.table + val check: Proof.context -> 'a table -> xstring * Position.T -> string + val get: 'a table -> string -> 'a val define: Proof.context -> bool -> naming -> binding * 'a -> 'a table -> string * 'a table val empty_table: string -> 'a table val merge_tables: 'a table * 'a table -> 'a table @@ -93,6 +95,8 @@ error ("Duplicate " ^ kind ^ " declaration " ^ print_entry true kind entry1 ^ " vs. " ^ print_entry true kind entry2); +fun undefined kind name = "Undefined " ^ kind ^ ": " ^ quote name; + (* datatype T *) @@ -367,8 +371,7 @@ |> fold (add_name name) accs |> map_name_space (fn (kind, internals, entries) => let - val _ = Symtab.defined entries name orelse - error ("Undefined " ^ kind ^ " " ^ quote name); + val _ = Symtab.defined entries name orelse error (undefined kind name); val entries' = entries |> Symtab.map_entry name (fn (externals, entry) => (Library.merge (op =) (externals, accs'), entry)) @@ -381,6 +384,18 @@ type 'a table = T * 'a Symtab.table; +fun check ctxt (space, tab) (xname, pos) = + let val name = intern space xname in + if Symtab.defined tab name + then (Context_Position.report ctxt pos (markup space name); name) + else error (undefined (kind_of space) name ^ Position.str_of pos) + end; + +fun get (space, tab) name = + (case Symtab.lookup tab name of + SOME x => x + | NONE => error (undefined (kind_of space) name)); + fun define ctxt strict naming (binding, x) (space, tab) = let val (name, space') = declare ctxt strict naming binding space in (name, (space', Symtab.update (name, x) tab)) end; diff -r 1ba52683512a -r bbce02fcba60 src/Pure/simplifier.ML --- a/src/Pure/simplifier.ML Sat Apr 23 16:30:00 2011 +0200 +++ b/src/Pure/simplifier.ML Sat Apr 23 17:02:12 2011 +0200 @@ -158,22 +158,8 @@ (* get simprocs *) -fun undef_simproc name = "Undefined simplification procedure: " ^ quote name; - -fun check_simproc ctxt (xname, pos) = - let - val (space, tab) = get_simprocs ctxt; - val name = Name_Space.intern space xname; - in - if Symtab.defined tab name then - (Context_Position.report ctxt pos (Name_Space.markup space name); name) - else error (undef_simproc name ^ Position.str_of pos) - end; - -fun the_simproc ctxt name = - (case Symtab.lookup (#2 (get_simprocs ctxt)) name of - SOME proc => proc - | NONE => error (undef_simproc name)); +fun check_simproc ctxt = Name_Space.check ctxt (get_simprocs ctxt); +val the_simproc = Name_Space.get o get_simprocs; val _ = ML_Antiquote.value "simproc"