# HG changeset patch
# User wenzelm
# Date 1376685571 -7200
# Node ID be27b6be8027e1fc52dda495e5352ba928b021f1
# Parent  8cbfbeb566a4c5e5c4b042fd3dbcdf19ba157897
more markup via Name_Space.check;
tuned signature;

diff -r 8cbfbeb566a4 -r be27b6be8027 src/Doc/antiquote_setup.ML
--- a/src/Doc/antiquote_setup.ML	Fri Aug 16 21:33:36 2013 +0200
+++ b/src/Doc/antiquote_setup.ML	Fri Aug 16 22:39:31 2013 +0200
@@ -146,13 +146,20 @@
 
 fun no_check _ _ = true;
 
-fun thy_check intern defined ctxt =
-  let val thy = Proof_Context.theory_of ctxt
-  in defined thy o intern thy end;
+fun thy_check check ctxt = can (check (Proof_Context.theory_of ctxt));
 
-fun check_tool name =
-  let val tool_dirs = map Path.explode ["~~/lib/Tools", "~~/src/Tools/jEdit/lib/Tools"]
-  in exists (fn dir => File.exists (Path.append dir (Path.basic name))) tool_dirs end;
+fun check_tool (name, pos) =
+  let
+    (* FIXME ISABELLE_TOOLS !? *)
+    val dirs = map Path.explode ["~~/lib/Tools", "~~/src/Tools/jEdit/lib/Tools"];
+    fun tool dir =
+      let val path = Path.append dir (Path.basic name)
+      in if File.exists path then SOME path else NONE end;
+  in
+    (case get_first tool dirs of
+      NONE => false
+    | SOME path => (Position.report pos (Markup.path (Path.implode path)); true))
+  end;
 
 val arg = enclose "{" "}" o clean_string;
 
@@ -160,8 +167,8 @@
   Thy_Output.antiquotation
     (Binding.name (translate (fn " " => "_" | c => c) kind ^
       (case index of NONE => "" | SOME true => "_def" | SOME false => "_ref")))
-    (Scan.lift (Scan.optional (Args.parens Args.name) "" -- Args.name))
-    (fn {context = ctxt, ...} => fn (logic, name) =>
+    (Scan.lift (Scan.optional (Args.parens Args.name) "" -- Parse.position Args.name))
+    (fn {context = ctxt, ...} => fn (logic, (name, pos)) =>
       let
         val hyper_name =
           "{" ^ Long_Name.append kind (Long_Name.append logic (clean_name name)) ^ "}";
@@ -174,7 +181,7 @@
           | SOME is_def =>
               "\\index" ^ (if is_def then "def" else "ref") ^ arg logic ^ arg kind ^ arg name);
       in
-        if check ctxt name then
+        if check ctxt (name, pos) then
           idx ^
           (Output.output name
             |> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}")
@@ -182,7 +189,7 @@
             |> (if Config.get ctxt Thy_Output.display
                 then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
                 else hyper o enclose "\\mbox{\\isa{" "}}"))
-        else error ("Bad " ^ kind ^ " " ^ quote name)
+        else error ("Bad " ^ kind ^ " " ^ quote name ^ Position.here pos)
       end);
 
 fun entity_antiqs check markup kind =
@@ -194,25 +201,22 @@
 
 val entity_setup =
   entity_antiqs no_check "" "syntax" #>
-  entity_antiqs (K (is_some o Keyword.command_keyword)) "isacommand" "command" #>
-  entity_antiqs (K Keyword.is_keyword) "isakeyword" "keyword" #>
-  entity_antiqs (K Keyword.is_keyword) "isakeyword" "element" #>
-  entity_antiqs (thy_check Method.intern Method.defined) "" "method" #>
-  entity_antiqs (thy_check Attrib.intern Attrib.defined) "" "attribute" #>
+  entity_antiqs (K (is_some o Keyword.command_keyword o #1)) "isacommand" "command" #>
+  entity_antiqs (K (Keyword.is_keyword o #1)) "isakeyword" "keyword" #>
+  entity_antiqs (K (Keyword.is_keyword o #1)) "isakeyword" "element" #>
+  entity_antiqs (thy_check Method.check) "" "method" #>
+  entity_antiqs (thy_check Attrib.check) "" "attribute" #>
   entity_antiqs no_check "" "fact" #>
   entity_antiqs no_check "" "variable" #>
   entity_antiqs no_check "" "case" #>
-  entity_antiqs (thy_check Thy_Output.intern_command Thy_Output.defined_command)
-    "" "antiquotation" #>
-  entity_antiqs (thy_check Thy_Output.intern_option Thy_Output.defined_option)
-    "" "antiquotation option" #>
+  entity_antiqs (thy_check Thy_Output.check_command) "" "antiquotation" #>
+  entity_antiqs (thy_check Thy_Output.check_option) "" "antiquotation option" #>
   entity_antiqs no_check "isatt" "setting" #>
   entity_antiqs no_check "isatt" "system option" #>
   entity_antiqs no_check "" "inference" #>
   entity_antiqs no_check "isatt" "executable" #>
   entity_antiqs (K check_tool) "isatool" "tool" #>
-  entity_antiqs (thy_check ML_Context.intern_antiq ML_Context.defined_antiq)
-    "" Markup.ML_antiquotationN;
+  entity_antiqs (thy_check ML_Context.check_antiq) "" Markup.ML_antiquotationN;
 
 end;
 
diff -r 8cbfbeb566a4 -r be27b6be8027 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Fri Aug 16 21:33:36 2013 +0200
+++ b/src/Pure/Isar/attrib.ML	Fri Aug 16 22:39:31 2013 +0200
@@ -11,10 +11,10 @@
   val empty_binding: binding
   val is_empty_binding: binding -> bool
   val print_attributes: theory -> unit
+  val check: theory -> xstring * Position.T -> string
   val intern: theory -> xstring -> string
   val intern_src: theory -> src -> src
   val pretty_attribs: Proof.context -> src list -> Pretty.T list
-  val defined: theory -> string -> bool
   val attribute: Proof.context -> src -> attribute
   val attribute_global: theory -> src -> attribute
   val attribute_cmd: Proof.context -> src -> attribute
@@ -114,6 +114,8 @@
 
 (* name space *)
 
+fun check thy = #1 o Name_Space.check (Context.Theory thy) (Attributes.get thy);
+
 val intern = Name_Space.intern o #1 o Attributes.get;
 val intern_src = Args.map_name o intern;
 
@@ -129,8 +131,6 @@
 
 (* get attributes *)
 
-val defined = Symtab.defined o #2 o Attributes.get;
-
 fun attribute_generic context =
   let
     val thy = Context.theory_of context;
diff -r 8cbfbeb566a4 -r be27b6be8027 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Fri Aug 16 21:33:36 2013 +0200
+++ b/src/Pure/Isar/method.ML	Fri Aug 16 22:39:31 2013 +0200
@@ -62,8 +62,8 @@
   val sorry_text: bool -> text
   val finish_text: text option * bool -> text
   val print_methods: theory -> unit
+  val check: theory -> xstring * Position.T -> string
   val intern: theory -> xstring -> string
-  val defined: theory -> string -> bool
   val method: theory -> src -> Proof.context -> method
   val method_i: theory -> src -> Proof.context -> method
   val syntax: 'a context_parser -> src -> Proof.context -> 'a * Proof.context
@@ -331,8 +331,9 @@
 
 (* get methods *)
 
+fun check thy = #1 o Name_Space.check (Context.Theory thy) (Methods.get thy);
+
 val intern = Name_Space.intern o #1 o Methods.get;
-val defined = Symtab.defined o #2 o Methods.get;
 
 fun method_i thy =
   let
diff -r 8cbfbeb566a4 -r be27b6be8027 src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Fri Aug 16 21:33:36 2013 +0200
+++ b/src/Pure/ML/ml_context.ML	Fri Aug 16 22:39:31 2013 +0200
@@ -25,8 +25,7 @@
   val ml_store_thm: string * thm -> unit
   type antiq = Proof.context -> (Proof.context -> string * string) * Proof.context
   val add_antiq: binding -> (Position.T -> antiq context_parser) -> theory -> theory
-  val intern_antiq: theory -> xstring -> string
-  val defined_antiq: theory -> string -> bool
+  val check_antiq: theory -> xstring * Position.T -> string
   val trace_raw: Config.raw
   val trace: bool Config.T
   val eval_antiquotes: ML_Lex.token Antiquote.antiquote list * Position.T ->
@@ -111,8 +110,7 @@
 fun add_antiq name scan thy = thy
   |> Antiq_Parsers.map (Name_Space.define (Context.Theory thy) true (name, scan) #> snd);
 
-val intern_antiq = Name_Space.intern o #1 o Antiq_Parsers.get;
-val defined_antiq = Symtab.defined o #2 o Antiq_Parsers.get;
+fun check_antiq thy = #1 o Name_Space.check (Context.Theory thy) (Antiq_Parsers.get thy);
 
 fun antiquotation src ctxt =
   let
diff -r 8cbfbeb566a4 -r be27b6be8027 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Fri Aug 16 21:33:36 2013 +0200
+++ b/src/Pure/Thy/thy_output.ML	Fri Aug 16 22:39:31 2013 +0200
@@ -14,10 +14,8 @@
   val modes: string Config.T
   val add_wrapper: ((unit -> string) -> unit -> string) -> Proof.context -> Proof.context
   val add_option: binding -> (string -> Proof.context -> Proof.context) -> theory -> theory
-  val intern_command: theory -> xstring -> string
-  val defined_command: theory -> string -> bool
-  val intern_option: theory -> xstring -> string
-  val defined_option: theory -> string -> bool
+  val check_command: theory -> xstring * Position.T -> string
+  val check_option: theory -> xstring * Position.T -> string
   val print_antiquotations: Proof.context -> unit
   val antiquotation: binding -> 'a context_parser ->
     ({source: Args.src, state: Toplevel.state, context: Proof.context} -> 'a -> string) ->
@@ -87,11 +85,9 @@
 fun add_option name opt thy = thy
   |> Antiquotations.map (apsnd (Name_Space.define (Context.Theory thy) true (name, opt) #> snd));
 
-val intern_command = Name_Space.intern o #1 o #1 o Antiquotations.get;
-val defined_command = Symtab.defined o #2 o #1 o Antiquotations.get;
+fun check_command thy = #1 o Name_Space.check (Context.Theory thy) (#1 (Antiquotations.get thy));
 
-val intern_option = Name_Space.intern o #1 o #2 o Antiquotations.get;
-val defined_option = Symtab.defined o #2 o #2 o Antiquotations.get;
+fun check_option thy = #1 o Name_Space.check (Context.Theory thy) (#2 (Antiquotations.get thy));
 
 fun command src state ctxt =
   let