more markup via Name_Space.check;
authorwenzelm
Fri Aug 16 22:39:31 2013 +0200 (2013-08-16)
changeset 53044be27b6be8027
parent 53043 8cbfbeb566a4
child 53045 4c297ee47c28
more markup via Name_Space.check;
tuned signature;
src/Doc/antiquote_setup.ML
src/Pure/Isar/attrib.ML
src/Pure/Isar/method.ML
src/Pure/ML/ml_context.ML
src/Pure/Thy/thy_output.ML
     1.1 --- a/src/Doc/antiquote_setup.ML	Fri Aug 16 21:33:36 2013 +0200
     1.2 +++ b/src/Doc/antiquote_setup.ML	Fri Aug 16 22:39:31 2013 +0200
     1.3 @@ -146,13 +146,20 @@
     1.4  
     1.5  fun no_check _ _ = true;
     1.6  
     1.7 -fun thy_check intern defined ctxt =
     1.8 -  let val thy = Proof_Context.theory_of ctxt
     1.9 -  in defined thy o intern thy end;
    1.10 +fun thy_check check ctxt = can (check (Proof_Context.theory_of ctxt));
    1.11  
    1.12 -fun check_tool name =
    1.13 -  let val tool_dirs = map Path.explode ["~~/lib/Tools", "~~/src/Tools/jEdit/lib/Tools"]
    1.14 -  in exists (fn dir => File.exists (Path.append dir (Path.basic name))) tool_dirs end;
    1.15 +fun check_tool (name, pos) =
    1.16 +  let
    1.17 +    (* FIXME ISABELLE_TOOLS !? *)
    1.18 +    val dirs = map Path.explode ["~~/lib/Tools", "~~/src/Tools/jEdit/lib/Tools"];
    1.19 +    fun tool dir =
    1.20 +      let val path = Path.append dir (Path.basic name)
    1.21 +      in if File.exists path then SOME path else NONE end;
    1.22 +  in
    1.23 +    (case get_first tool dirs of
    1.24 +      NONE => false
    1.25 +    | SOME path => (Position.report pos (Markup.path (Path.implode path)); true))
    1.26 +  end;
    1.27  
    1.28  val arg = enclose "{" "}" o clean_string;
    1.29  
    1.30 @@ -160,8 +167,8 @@
    1.31    Thy_Output.antiquotation
    1.32      (Binding.name (translate (fn " " => "_" | c => c) kind ^
    1.33        (case index of NONE => "" | SOME true => "_def" | SOME false => "_ref")))
    1.34 -    (Scan.lift (Scan.optional (Args.parens Args.name) "" -- Args.name))
    1.35 -    (fn {context = ctxt, ...} => fn (logic, name) =>
    1.36 +    (Scan.lift (Scan.optional (Args.parens Args.name) "" -- Parse.position Args.name))
    1.37 +    (fn {context = ctxt, ...} => fn (logic, (name, pos)) =>
    1.38        let
    1.39          val hyper_name =
    1.40            "{" ^ Long_Name.append kind (Long_Name.append logic (clean_name name)) ^ "}";
    1.41 @@ -174,7 +181,7 @@
    1.42            | SOME is_def =>
    1.43                "\\index" ^ (if is_def then "def" else "ref") ^ arg logic ^ arg kind ^ arg name);
    1.44        in
    1.45 -        if check ctxt name then
    1.46 +        if check ctxt (name, pos) then
    1.47            idx ^
    1.48            (Output.output name
    1.49              |> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}")
    1.50 @@ -182,7 +189,7 @@
    1.51              |> (if Config.get ctxt Thy_Output.display
    1.52                  then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
    1.53                  else hyper o enclose "\\mbox{\\isa{" "}}"))
    1.54 -        else error ("Bad " ^ kind ^ " " ^ quote name)
    1.55 +        else error ("Bad " ^ kind ^ " " ^ quote name ^ Position.here pos)
    1.56        end);
    1.57  
    1.58  fun entity_antiqs check markup kind =
    1.59 @@ -194,25 +201,22 @@
    1.60  
    1.61  val entity_setup =
    1.62    entity_antiqs no_check "" "syntax" #>
    1.63 -  entity_antiqs (K (is_some o Keyword.command_keyword)) "isacommand" "command" #>
    1.64 -  entity_antiqs (K Keyword.is_keyword) "isakeyword" "keyword" #>
    1.65 -  entity_antiqs (K Keyword.is_keyword) "isakeyword" "element" #>
    1.66 -  entity_antiqs (thy_check Method.intern Method.defined) "" "method" #>
    1.67 -  entity_antiqs (thy_check Attrib.intern Attrib.defined) "" "attribute" #>
    1.68 +  entity_antiqs (K (is_some o Keyword.command_keyword o #1)) "isacommand" "command" #>
    1.69 +  entity_antiqs (K (Keyword.is_keyword o #1)) "isakeyword" "keyword" #>
    1.70 +  entity_antiqs (K (Keyword.is_keyword o #1)) "isakeyword" "element" #>
    1.71 +  entity_antiqs (thy_check Method.check) "" "method" #>
    1.72 +  entity_antiqs (thy_check Attrib.check) "" "attribute" #>
    1.73    entity_antiqs no_check "" "fact" #>
    1.74    entity_antiqs no_check "" "variable" #>
    1.75    entity_antiqs no_check "" "case" #>
    1.76 -  entity_antiqs (thy_check Thy_Output.intern_command Thy_Output.defined_command)
    1.77 -    "" "antiquotation" #>
    1.78 -  entity_antiqs (thy_check Thy_Output.intern_option Thy_Output.defined_option)
    1.79 -    "" "antiquotation option" #>
    1.80 +  entity_antiqs (thy_check Thy_Output.check_command) "" "antiquotation" #>
    1.81 +  entity_antiqs (thy_check Thy_Output.check_option) "" "antiquotation option" #>
    1.82    entity_antiqs no_check "isatt" "setting" #>
    1.83    entity_antiqs no_check "isatt" "system option" #>
    1.84    entity_antiqs no_check "" "inference" #>
    1.85    entity_antiqs no_check "isatt" "executable" #>
    1.86    entity_antiqs (K check_tool) "isatool" "tool" #>
    1.87 -  entity_antiqs (thy_check ML_Context.intern_antiq ML_Context.defined_antiq)
    1.88 -    "" Markup.ML_antiquotationN;
    1.89 +  entity_antiqs (thy_check ML_Context.check_antiq) "" Markup.ML_antiquotationN;
    1.90  
    1.91  end;
    1.92  
     2.1 --- a/src/Pure/Isar/attrib.ML	Fri Aug 16 21:33:36 2013 +0200
     2.2 +++ b/src/Pure/Isar/attrib.ML	Fri Aug 16 22:39:31 2013 +0200
     2.3 @@ -11,10 +11,10 @@
     2.4    val empty_binding: binding
     2.5    val is_empty_binding: binding -> bool
     2.6    val print_attributes: theory -> unit
     2.7 +  val check: theory -> xstring * Position.T -> string
     2.8    val intern: theory -> xstring -> string
     2.9    val intern_src: theory -> src -> src
    2.10    val pretty_attribs: Proof.context -> src list -> Pretty.T list
    2.11 -  val defined: theory -> string -> bool
    2.12    val attribute: Proof.context -> src -> attribute
    2.13    val attribute_global: theory -> src -> attribute
    2.14    val attribute_cmd: Proof.context -> src -> attribute
    2.15 @@ -114,6 +114,8 @@
    2.16  
    2.17  (* name space *)
    2.18  
    2.19 +fun check thy = #1 o Name_Space.check (Context.Theory thy) (Attributes.get thy);
    2.20 +
    2.21  val intern = Name_Space.intern o #1 o Attributes.get;
    2.22  val intern_src = Args.map_name o intern;
    2.23  
    2.24 @@ -129,8 +131,6 @@
    2.25  
    2.26  (* get attributes *)
    2.27  
    2.28 -val defined = Symtab.defined o #2 o Attributes.get;
    2.29 -
    2.30  fun attribute_generic context =
    2.31    let
    2.32      val thy = Context.theory_of context;
     3.1 --- a/src/Pure/Isar/method.ML	Fri Aug 16 21:33:36 2013 +0200
     3.2 +++ b/src/Pure/Isar/method.ML	Fri Aug 16 22:39:31 2013 +0200
     3.3 @@ -62,8 +62,8 @@
     3.4    val sorry_text: bool -> text
     3.5    val finish_text: text option * bool -> text
     3.6    val print_methods: theory -> unit
     3.7 +  val check: theory -> xstring * Position.T -> string
     3.8    val intern: theory -> xstring -> string
     3.9 -  val defined: theory -> string -> bool
    3.10    val method: theory -> src -> Proof.context -> method
    3.11    val method_i: theory -> src -> Proof.context -> method
    3.12    val syntax: 'a context_parser -> src -> Proof.context -> 'a * Proof.context
    3.13 @@ -331,8 +331,9 @@
    3.14  
    3.15  (* get methods *)
    3.16  
    3.17 +fun check thy = #1 o Name_Space.check (Context.Theory thy) (Methods.get thy);
    3.18 +
    3.19  val intern = Name_Space.intern o #1 o Methods.get;
    3.20 -val defined = Symtab.defined o #2 o Methods.get;
    3.21  
    3.22  fun method_i thy =
    3.23    let
     4.1 --- a/src/Pure/ML/ml_context.ML	Fri Aug 16 21:33:36 2013 +0200
     4.2 +++ b/src/Pure/ML/ml_context.ML	Fri Aug 16 22:39:31 2013 +0200
     4.3 @@ -25,8 +25,7 @@
     4.4    val ml_store_thm: string * thm -> unit
     4.5    type antiq = Proof.context -> (Proof.context -> string * string) * Proof.context
     4.6    val add_antiq: binding -> (Position.T -> antiq context_parser) -> theory -> theory
     4.7 -  val intern_antiq: theory -> xstring -> string
     4.8 -  val defined_antiq: theory -> string -> bool
     4.9 +  val check_antiq: theory -> xstring * Position.T -> string
    4.10    val trace_raw: Config.raw
    4.11    val trace: bool Config.T
    4.12    val eval_antiquotes: ML_Lex.token Antiquote.antiquote list * Position.T ->
    4.13 @@ -111,8 +110,7 @@
    4.14  fun add_antiq name scan thy = thy
    4.15    |> Antiq_Parsers.map (Name_Space.define (Context.Theory thy) true (name, scan) #> snd);
    4.16  
    4.17 -val intern_antiq = Name_Space.intern o #1 o Antiq_Parsers.get;
    4.18 -val defined_antiq = Symtab.defined o #2 o Antiq_Parsers.get;
    4.19 +fun check_antiq thy = #1 o Name_Space.check (Context.Theory thy) (Antiq_Parsers.get thy);
    4.20  
    4.21  fun antiquotation src ctxt =
    4.22    let
     5.1 --- a/src/Pure/Thy/thy_output.ML	Fri Aug 16 21:33:36 2013 +0200
     5.2 +++ b/src/Pure/Thy/thy_output.ML	Fri Aug 16 22:39:31 2013 +0200
     5.3 @@ -14,10 +14,8 @@
     5.4    val modes: string Config.T
     5.5    val add_wrapper: ((unit -> string) -> unit -> string) -> Proof.context -> Proof.context
     5.6    val add_option: binding -> (string -> Proof.context -> Proof.context) -> theory -> theory
     5.7 -  val intern_command: theory -> xstring -> string
     5.8 -  val defined_command: theory -> string -> bool
     5.9 -  val intern_option: theory -> xstring -> string
    5.10 -  val defined_option: theory -> string -> bool
    5.11 +  val check_command: theory -> xstring * Position.T -> string
    5.12 +  val check_option: theory -> xstring * Position.T -> string
    5.13    val print_antiquotations: Proof.context -> unit
    5.14    val antiquotation: binding -> 'a context_parser ->
    5.15      ({source: Args.src, state: Toplevel.state, context: Proof.context} -> 'a -> string) ->
    5.16 @@ -87,11 +85,9 @@
    5.17  fun add_option name opt thy = thy
    5.18    |> Antiquotations.map (apsnd (Name_Space.define (Context.Theory thy) true (name, opt) #> snd));
    5.19  
    5.20 -val intern_command = Name_Space.intern o #1 o #1 o Antiquotations.get;
    5.21 -val defined_command = Symtab.defined o #2 o #1 o Antiquotations.get;
    5.22 +fun check_command thy = #1 o Name_Space.check (Context.Theory thy) (#1 (Antiquotations.get thy));
    5.23  
    5.24 -val intern_option = Name_Space.intern o #1 o #2 o Antiquotations.get;
    5.25 -val defined_option = Symtab.defined o #2 o #2 o Antiquotations.get;
    5.26 +fun check_option thy = #1 o Name_Space.check (Context.Theory thy) (#2 (Antiquotations.get thy));
    5.27  
    5.28  fun command src state ctxt =
    5.29    let