# HG changeset patch
# User wenzelm
# Date 1394471183 -3600
# Node ID b034b9f0fa2a956804f67ac5070fdc777b5c6e8d
# Parent  2e3329b89383b02046a7d3386b4e0f00484791b4
clarified Args.check_src: retain name space information for error output;
tuned signature;

diff -r 2e3329b89383 -r b034b9f0fa2a src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Mon Mar 10 17:52:30 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Mon Mar 10 18:06:23 2014 +0100
@@ -162,7 +162,7 @@
   let
     val ths = Attrib.eval_thms ctxt [xthm]
     val bracket =
-      map (enclose "[" "]" o Pretty.str_of o Args.pretty_src Pretty.str ctxt) args
+      map (enclose "[" "]" o Pretty.str_of o Args.pretty_src ctxt) args
       |> implode
     fun nth_name j =
       (case xref of
diff -r 2e3329b89383 -r b034b9f0fa2a src/HOL/Tools/recdef.ML
--- a/src/HOL/Tools/recdef.ML	Mon Mar 10 17:52:30 2014 +0100
+++ b/src/HOL/Tools/recdef.ML	Mon Mar 10 18:06:23 2014 +0100
@@ -164,7 +164,7 @@
     val ctxt =
       (case opt_src of
         NONE => ctxt0
-      | SOME src => #2 (Method.syntax (Method.sections recdef_modifiers) src ctxt0));
+      | SOME src => #2 (Args.syntax (Method.sections recdef_modifiers) src ctxt0));
     val {simps, congs, wfs} = get_hints ctxt;
     val ctxt' = ctxt addsimps simps |> Simplifier.del_cong @{thm imp_cong};
   in (ctxt', rev (map snd congs), wfs) end;
diff -r 2e3329b89383 -r b034b9f0fa2a src/HOL/Tools/try0.ML
--- a/src/HOL/Tools/try0.ML	Mon Mar 10 17:52:30 2014 +0100
+++ b/src/HOL/Tools/try0.ML	Mon Mar 10 18:06:23 2014 +0100
@@ -172,7 +172,7 @@
 
 fun string_of_xthm (xref, args) =
   Facts.string_of_ref xref ^
-  implode (map (enclose "[" "]" o Pretty.str_of o Args.pretty_src Pretty.str @{context}) args);
+  implode (map (enclose "[" "]" o Pretty.str_of o Args.pretty_src @{context}) args);
 
 val parse_fact_refs =
   Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) (Parse_Spec.xthm >> string_of_xthm));
diff -r 2e3329b89383 -r b034b9f0fa2a src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Mon Mar 10 17:52:30 2014 +0100
+++ b/src/Pure/Isar/args.ML	Mon Mar 10 18:06:23 2014 +0100
@@ -12,8 +12,8 @@
   val name_of_src: src -> string * Position.T
   val args_of_src: src -> Token.T list
   val unparse_src: src -> string list
-  val pretty_src: (string -> Pretty.T) -> Proof.context -> src -> Pretty.T
-  val check_src: Context.generic -> 'a Name_Space.table -> src -> src * 'a
+  val pretty_src: Proof.context -> src -> Pretty.T
+  val check_src: Proof.context -> 'a Name_Space.table -> src -> src * 'a
   val transform_values: morphism -> src -> src
   val init_assignable: src -> src
   val closure: src -> src
@@ -67,8 +67,8 @@
   val opt_attribs: (xstring * Position.T -> string) -> src list parser
   val thm_name: (xstring * Position.T -> string) -> string -> (binding * src list) parser
   val opt_thm_name: (xstring * Position.T -> string) -> string -> (binding * src list) parser
-  val syntax: string -> 'a context_parser -> src -> Context.generic -> 'a * Context.generic
-  val context_syntax: string -> 'a context_parser -> src -> Proof.context -> 'a * Proof.context
+  val syntax_generic: 'a context_parser -> src -> Context.generic -> 'a * Context.generic
+  val syntax: 'a context_parser -> src -> Proof.context -> 'a * Proof.context
 end;
 
 structure Args: ARGS =
@@ -76,18 +76,28 @@
 
 (** datatype src **)
 
-datatype src = Src of (string * Position.T) * Token.T list;
+datatype src =
+  Src of
+   {name: string * Position.T,
+    args: Token.T list,
+    output_info: (string * Markup.T) option};
 
-val src = curry Src;
+fun src name args = Src {name = name, args = args, output_info = NONE};
 
-fun map_args f (Src (name, args)) = Src (name, map f args);
+fun map_args f (Src {name, args, output_info}) =
+  Src {name = name, args = map f args, output_info = output_info};
 
-fun name_of_src (Src (name, _)) = name;
-fun args_of_src (Src (_, args)) = args;
+fun name_of_src (Src {name, ...}) = name;
+fun args_of_src (Src {args, ...}) = args;
+
+fun unparse_src (Src {args, ...}) = map Token.unparse args;
 
-fun unparse_src (Src (_, args)) = map Token.unparse args;
+fun pretty_name (Src {name = (name, _), output_info, ...}) =
+  (case output_info of
+    NONE => Pretty.str name
+  | SOME (_, markup) => Pretty.mark_str (markup, name));
 
-fun pretty_src pretty_name ctxt src =
+fun pretty_src ctxt src =
   let
     val prt_thm = Pretty.backquote o Display.pretty_thm ctxt;
     fun prt arg =
@@ -98,15 +108,18 @@
       | SOME (Token.Term t) => Syntax.pretty_term ctxt t
       | SOME (Token.Fact ths) => Pretty.enclose "(" ")" (Pretty.breaks (map prt_thm ths))
       | _ => Pretty.mark_str (Token.markup arg, Token.unparse arg));
-    val Src ((name, _), args) = src;
-  in Pretty.block (Pretty.breaks (pretty_name name :: map prt args)) end;
+  in Pretty.block (Pretty.breaks (pretty_name src :: map prt (args_of_src src))) end;
 
 
 (* check *)
 
-fun check_src context table (Src ((xname, pos), args)) =
-  let val (name, x) = Name_Space.check context table (xname, pos)
-  in (Src ((name, pos), args), x) end;
+fun check_src ctxt table (Src {name = (xname, pos), args, output_info = _}) =
+  let
+    val (name, x) = Name_Space.check (Context.Proof ctxt) table (xname, pos);
+    val space = Name_Space.space_of_table table;
+    val kind = Name_Space.kind_of space;
+    val markup = Name_Space.markup space name;
+  in (Src {name = (name, pos), args = args, output_info = SOME (kind, markup)}, x) end;
 
 
 (* values *)
@@ -296,9 +309,13 @@
 
 (** syntax wrapper **)
 
-fun syntax kind scan (Src ((name, pos), args0)) context =
+fun syntax_generic scan (Src {name = (name, pos), args = args0, output_info}) context =
   let
     val args1 = map Token.init_assignable args0;
+    fun print_name () =
+      (case output_info of
+        NONE => quote name
+      | SOME (kind, markup) => kind ^ " " ^ Markup.markup markup (quote name));
     fun reported_text () =
       if Context_Position.is_visible_generic context then
         maps (Token.reports_of_value o Token.closure) args1
@@ -309,12 +326,11 @@
     (case Scan.error (Scan.finite' Token.stopper (Scan.option scan)) (context, args1) of
       (SOME x, (context', [])) => (Output.report (reported_text ()); (x, context'))
     | (_, (_, args2)) =>
-        error ("Bad arguments for " ^ kind ^ " " ^ quote name ^ Position.here pos ^
+        error ("Bad arguments for " ^ print_name () ^ Position.here pos ^
           (if null args2 then "" else ":\n  " ^ space_implode " " (map Token.print args2)) ^
           Markup.markup_report (reported_text ())))
   end;
 
-fun context_syntax kind scan src =
-  apsnd Context.the_proof o syntax kind scan src o Context.Proof;
+fun syntax scan src = apsnd Context.the_proof o syntax_generic scan src o Context.Proof;
 
 end;
diff -r 2e3329b89383 -r b034b9f0fa2a src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Mon Mar 10 17:52:30 2014 +0100
+++ b/src/Pure/Isar/attrib.ML	Mon Mar 10 18:06:23 2014 +0100
@@ -12,7 +12,6 @@
   val is_empty_binding: binding -> bool
   val print_attributes: Proof.context -> unit
   val check_name_generic: Context.generic -> xstring * Position.T -> string
-  val check_src_generic: Context.generic -> src -> src
   val check_name: Proof.context -> xstring * Position.T -> string
   val check_src: Proof.context -> src -> src
   val pretty_attribs: Proof.context -> src list -> Pretty.T list
@@ -118,19 +117,15 @@
 (* check *)
 
 fun check_name_generic context = #1 o Name_Space.check context (get_attributes context);
-fun check_src_generic context src = #1 (Args.check_src context (get_attributes context) src);
+val check_name = check_name_generic o Context.Proof;
 
-val check_name = check_name_generic o Context.Proof;
-val check_src = check_src_generic o Context.Proof;
+fun check_src ctxt src = #1 (Args.check_src ctxt (get_attributes (Context.Proof ctxt)) src);
 
 
 (* pretty printing *)
 
-fun pretty_attrib ctxt =
-  Args.pretty_src (Name_Space.pretty ctxt (attribute_space ctxt)) ctxt;
-
 fun pretty_attribs _ [] = []
-  | pretty_attribs ctxt srcs = [Pretty.enum "," "[" "]" (map (pretty_attrib ctxt) srcs)];
+  | pretty_attribs ctxt srcs = [Pretty.enum "," "[" "]" (map (Args.pretty_src ctxt) srcs)];
 
 
 (* get attributes *)
@@ -143,7 +138,7 @@
 val attribute_global = attribute_generic o Context.Theory;
 
 fun attribute_cmd ctxt = attribute ctxt o check_src ctxt;
-fun attribute_cmd_global thy = attribute_global thy o check_src_generic (Context.Theory thy);
+fun attribute_cmd_global thy = attribute_global thy o check_src (Proof_Context.init_global thy);
 
 
 (* attributed declarations *)
@@ -174,11 +169,10 @@
 
 (* attribute setup *)
 
-fun syntax scan = Args.syntax "attribute" scan;
-
 fun setup name scan =
   add_attribute name
-    (fn src => fn (ctxt, th) => let val (a, ctxt') = syntax scan src ctxt in a (ctxt', th) end);
+    (fn src => fn (ctxt, th) =>
+      let val (a, ctxt') = Args.syntax_generic scan src ctxt in a (ctxt', th) end);
 
 fun attribute_setup name source cmt =
   Context.theory_map (ML_Context.expression (#pos source)
diff -r 2e3329b89383 -r b034b9f0fa2a src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Mon Mar 10 17:52:30 2014 +0100
+++ b/src/Pure/Isar/method.ML	Mon Mar 10 18:06:23 2014 +0100
@@ -67,7 +67,6 @@
   val check_src: Proof.context -> src -> src
   val method: Proof.context -> src -> Proof.context -> method
   val method_cmd: Proof.context -> src -> Proof.context -> method
-  val syntax: 'a context_parser -> src -> Proof.context -> 'a * Proof.context
   val setup: binding -> (Proof.context -> method) context_parser -> string -> theory -> theory
   val method_setup: bstring * Position.T -> Symbol_Pos.source -> string -> theory -> theory
   type modifier = (Proof.context -> Proof.context) * attribute
@@ -340,7 +339,7 @@
 (* check *)
 
 fun check_name ctxt = #1 o Name_Space.check (Context.Proof ctxt) (get_methods ctxt);
-fun check_src ctxt src = #1 (Args.check_src (Context.Proof ctxt) (get_methods ctxt) src);
+fun check_src ctxt src = #1 (Args.check_src ctxt (get_methods ctxt) src);
 
 
 (* get methods *)
@@ -354,11 +353,9 @@
 
 (* method setup *)
 
-fun syntax scan = Args.context_syntax "method" scan;
-
 fun setup name scan =
   add_method name
-    (fn src => fn ctxt => let val (m, ctxt') = syntax scan src ctxt in m ctxt' end);
+    (fn src => fn ctxt => let val (m, ctxt') = Args.syntax scan src ctxt in m ctxt' end);
 
 fun method_setup name source cmt =
   Context.theory_map (ML_Context.expression (#pos source)
diff -r 2e3329b89383 -r b034b9f0fa2a src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Mon Mar 10 17:52:30 2014 +0100
+++ b/src/Pure/ML/ml_context.ML	Mon Mar 10 18:06:23 2014 +0100
@@ -115,8 +115,8 @@
 fun check_antiq ctxt = #1 o Name_Space.check (Context.Proof ctxt) (get_antiqs ctxt);
 
 fun antiquotation src ctxt =
-  let val (src', scan) = Args.check_src (Context.Proof ctxt) (get_antiqs ctxt) src
-  in Args.context_syntax Markup.ML_antiquotationN scan src' ctxt end;
+  let val (src', scan) = Args.check_src ctxt (get_antiqs ctxt) src
+  in Args.syntax scan src' ctxt end;
 
 
 (* parsing and evaluation *)
diff -r 2e3329b89383 -r b034b9f0fa2a src/Pure/Thy/term_style.ML
--- a/src/Pure/Thy/term_style.ML	Mon Mar 10 17:52:30 2014 +0100
+++ b/src/Pure/Thy/term_style.ML	Mon Mar 10 18:06:23 2014 +0100
@@ -35,8 +35,8 @@
 fun parse_single ctxt =
   Parse.position Parse.xname -- Args.parse >> (fn (name, args) =>
     let
-      val (src, parse) = Args.check_src (Context.Proof ctxt) (get_data ctxt) (Args.src name args);
-      val (f, _) = Args.context_syntax "antiquotation_style" (Scan.lift parse) src ctxt;
+      val (src, parse) = Args.check_src ctxt (get_data ctxt) (Args.src name args);
+      val (f, _) = Args.syntax (Scan.lift parse) src ctxt;
     in f ctxt end);
 
 val parse = Args.context :|-- (fn ctxt => Scan.lift
diff -r 2e3329b89383 -r b034b9f0fa2a src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Mon Mar 10 17:52:30 2014 +0100
+++ b/src/Pure/Thy/thy_output.ML	Mon Mar 10 18:06:23 2014 +0100
@@ -92,7 +92,7 @@
 fun check_option ctxt = #1 o Name_Space.check (Context.Proof ctxt) (#2 (get_antiquotations ctxt));
 
 fun command src state ctxt =
-  let val (src', f) = Args.check_src (Context.Proof ctxt) (#1 (get_antiquotations ctxt)) src
+  let val (src', f) = Args.check_src ctxt (#1 (get_antiquotations ctxt)) src
   in f src' state ctxt end;
 
 fun option ((xname, pos), s) ctxt =
@@ -115,7 +115,7 @@
 fun antiquotation name scan out =
   add_command name
     (fn src => fn state => fn ctxt =>
-      let val (x, ctxt') = Args.context_syntax "document antiquotation" scan src ctxt
+      let val (x, ctxt') = Args.syntax scan src ctxt
       in out {source = src, state = state, context = ctxt'} x end);