# HG changeset patch
# User wenzelm
# Date 1394465407 -3600
# Node ID 8bedca4bd5a3f40f89a0f139c0587025e9cbe105
# Parent  422024102d9d8cb5d1dc39b9785d20848a9e185e
clarified Args.src: more abstract type, position refers to name only;
prefer self-contained Args.check_src;

diff -r 422024102d9d -r 8bedca4bd5a3 src/HOL/Tools/Lifting/lifting_setup.ML
--- a/src/HOL/Tools/Lifting/lifting_setup.ML	Mon Mar 10 15:30:29 2014 +0100
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Mon Mar 10 16:30:07 2014 +0100
@@ -223,7 +223,7 @@
     val dummy_thm = Thm.transfer thy Drule.dummy_thm
     val pointer = Outer_Syntax.scan Position.none bundle_name
     val restore_lifting_att = 
-      ([dummy_thm], [Args.src (("Lifting.lifting_restore_internal", pointer), Position.none)])
+      ([dummy_thm], [Args.src ("Lifting.lifting_restore_internal", Position.none) pointer])
   in
     lthy 
       |> Local_Theory.declaration {syntax = false, pervasive = true}
@@ -959,7 +959,7 @@
     case bundle of
       [(_, [arg_src])] => 
         (let
-          val ((_, tokens), _) = Args.dest_src arg_src
+          val tokens = Args.args_of_src arg_src
         in
           (fst (Args.name tokens))
           handle _ => error "The provided bundle is not a lifting bundle."
diff -r 422024102d9d -r 8bedca4bd5a3 src/HOL/Tools/recdef.ML
--- a/src/HOL/Tools/recdef.ML	Mon Mar 10 15:30:29 2014 +0100
+++ b/src/HOL/Tools/recdef.ML	Mon Mar 10 16:30:07 2014 +0100
@@ -290,7 +290,8 @@
 
 val hints =
   @{keyword "("} |--
-    Parse.!!! (Parse.position (@{keyword "hints"} -- Args.parse) --| @{keyword ")"}) >> Args.src;
+    Parse.!!! (Parse.position @{keyword "hints"} -- Args.parse --| @{keyword ")"})
+  >> uncurry Args.src;
 
 val recdef_decl =
   Scan.optional
diff -r 422024102d9d -r 8bedca4bd5a3 src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Mon Mar 10 15:30:29 2014 +0100
+++ b/src/Pure/Isar/args.ML	Mon Mar 10 16:30:07 2014 +0100
@@ -8,11 +8,12 @@
 signature ARGS =
 sig
   type src
-  val src: (string * Token.T list) * Position.T -> src
-  val dest_src: src -> (string * Token.T list) * Position.T
+  val src: xstring * Position.T -> Token.T list -> src
+  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 map_name: (string -> string) -> src -> src
+  val check_src: Context.generic -> 'a Name_Space.table -> src -> src * 'a
   val transform_values: morphism -> src -> src
   val init_assignable: src -> src
   val closure: src -> src
@@ -75,12 +76,16 @@
 
 (** datatype src **)
 
-datatype src = Src of (string * Token.T list) * Position.T;
+datatype src = Src of (string * Position.T) * Token.T list;
+
+val src = curry Src;
 
-val src = Src;
-fun dest_src (Src src) = src;
+fun map_args f (Src (name, args)) = Src (name, map f args);
 
-fun unparse_src (Src ((_, toks), _)) = map Token.unparse toks;
+fun name_of_src (Src (name, _)) = name;
+fun args_of_src (Src (_, args)) = args;
+
+fun unparse_src (Src (_, args)) = map Token.unparse args;
 
 fun pretty_src pretty_name ctxt src =
   let
@@ -93,11 +98,15 @@
       | 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 (name, args) = #1 (dest_src src);
+    val Src ((name, _), args) = src;
   in Pretty.block (Pretty.breaks (pretty_name name :: map prt args)) end;
 
-fun map_name f (Src ((s, args), pos)) = Src ((f s, args), pos);
-fun map_args f (Src ((s, args), pos)) = Src ((s, map f args), pos);
+
+(* 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;
 
 
 (* values *)
@@ -268,7 +277,7 @@
   let
     fun intern tok = check (Token.content_of tok, Token.pos_of tok);
     val attrib_name = internal_text || (symbolic || named) >> evaluate Token.Text intern;
-    val attrib = Parse.position (attrib_name -- Parse.!!! parse) >> src;
+    val attrib = Parse.position attrib_name -- Parse.!!! parse >> uncurry src;
   in $$$ "[" |-- Parse.!!! (Parse.list attrib --| $$$ "]") end;
 
 fun opt_attribs check = Scan.optional (attribs check) [];
@@ -287,7 +296,7 @@
 
 (** syntax wrapper **)
 
-fun syntax kind scan (Src ((s, args0), pos)) context =
+fun syntax kind scan (Src ((name, pos), args0)) context =
   let
     val args1 = map Token.init_assignable args0;
     fun reported_text () =
@@ -300,7 +309,7 @@
     (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 s ^ Position.here pos ^
+        error ("Bad arguments for " ^ kind ^ " " ^ quote name ^ Position.here pos ^
           (if null args2 then "" else ":\n  " ^ space_implode " " (map Token.print args2)) ^
           Markup.markup_report (reported_text ())))
   end;
diff -r 422024102d9d -r 8bedca4bd5a3 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Mon Mar 10 15:30:29 2014 +0100
+++ b/src/Pure/Isar/attrib.ML	Mon Mar 10 16:30:07 2014 +0100
@@ -118,12 +118,7 @@
 (* check *)
 
 fun check_name_generic context = #1 o Name_Space.check context (get_attributes context);
-
-fun check_src_generic context src =
-  let
-    val ((xname, toks), pos) = Args.dest_src src;
-    val name = check_name_generic context (xname, pos);
-  in Args.src ((name, toks), pos) end;
+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_src = check_src_generic o Context.Proof;
@@ -141,13 +136,8 @@
 (* get attributes *)
 
 fun attribute_generic context =
-  let val table = get_attributes context in
-    fn src =>
-      let
-        val ((name, _), _) = Args.dest_src src;
-        val (att, _) = Name_Space.get table name;
-      in att src end
-  end;
+  let val table = get_attributes context
+  in fn src => #1 (Name_Space.get table (#1 (Args.name_of_src src))) src end;
 
 val attribute = attribute_generic o Context.Proof;
 val attribute_global = attribute_generic o Context.Theory;
@@ -201,7 +191,7 @@
 
 (* internal attribute *)
 
-fun internal att = Args.src (("Pure.attribute", [Token.mk_attribute att]), Position.none);
+fun internal att = Args.src ("Pure.attribute", Position.none) [Token.mk_attribute att];
 
 val _ = Theory.setup
  (setup (Binding.name "attribute") (Scan.lift Args.internal_attribute >> Morphism.form)
@@ -273,7 +263,7 @@
   in (src2, result) end;
 
 fun err msg src =
-  let val ((name, _), pos) = Args.dest_src src
+  let val (name, pos) = Args.name_of_src src
   in error (msg ^ " " ^ quote name ^ Position.here pos) end;
 
 fun eval src ((th, dyn), (decls, context)) =
diff -r 422024102d9d -r 8bedca4bd5a3 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Mon Mar 10 15:30:29 2014 +0100
+++ b/src/Pure/Isar/method.ML	Mon Mar 10 16:30:07 2014 +0100
@@ -300,7 +300,7 @@
 
 fun primitive_text r = Basic (SIMPLE_METHOD o PRIMITIVE o r);
 val succeed_text = Basic (K succeed);
-val default_text = Source (Args.src (("default", []), Position.none));
+val default_text = Source (Args.src ("default", Position.none) []);
 val this_text = Basic (K this);
 val done_text = Basic (K (SIMPLE_METHOD all_tac));
 fun sorry_text int = Basic (fn ctxt => cheating ctxt int);
@@ -340,24 +340,14 @@
 (* check *)
 
 fun check_name ctxt = #1 o Name_Space.check (Context.Proof ctxt) (get_methods ctxt);
-
-fun check_src ctxt src =
-  let
-    val ((xname, toks), pos) = Args.dest_src src;
-    val name = check_name ctxt (xname, pos);
-  in Args.src ((name, toks), pos) end;
+fun check_src ctxt src = #1 (Args.check_src (Context.Proof ctxt) (get_methods ctxt) src);
 
 
 (* get methods *)
 
 fun method ctxt =
-  let val table = get_methods ctxt in
-    fn src =>
-      let
-        val ((name, _), _) = Args.dest_src src;
-        val (meth, _) = Name_Space.get table name;
-      in meth src end
-  end;
+  let val table = get_methods ctxt
+  in fn src => #1 (Name_Space.get table (#1 (Args.name_of_src src))) src end;
 
 fun method_cmd ctxt = method ctxt o check_src ctxt;
 
@@ -456,9 +446,9 @@
 local
 
 fun meth4 x =
- (Parse.position (Parse.xname >> rpair []) >> (Source o Args.src) ||
+ (Parse.position Parse.xname >> (fn name => Source (Args.src name [])) ||
   Scan.ahead Parse.cartouche |-- Parse.not_eof >> (fn tok =>
-    Source (Args.src (("cartouche", [tok]), Token.pos_of tok))) ||
+    Source (Args.src ("cartouche", Token.pos_of tok) [tok])) ||
   Parse.$$$ "(" |-- Parse.!!! (meth0 --| Parse.$$$ ")")) x
 and meth3 x =
  (meth4 -- Parse.position (Parse.$$$ "?")
@@ -471,7 +461,7 @@
         Select_Goals (combinator_info [pos1, pos2], n, m)) ||
   meth4) x
 and meth2 x =
- (Parse.position (Parse.xname -- Args.parse1 is_symid_meth) >> (Source o Args.src) ||
+ (Parse.position Parse.xname -- Args.parse1 is_symid_meth >> (Source o uncurry Args.src) ||
   meth3) x
 and meth1 x =
   (Parse.enum1_positions "," meth2
diff -r 422024102d9d -r 8bedca4bd5a3 src/Pure/Isar/parse_spec.ML
--- a/src/Pure/Isar/parse_spec.ML	Mon Mar 10 15:30:29 2014 +0100
+++ b/src/Pure/Isar/parse_spec.ML	Mon Mar 10 16:30:07 2014 +0100
@@ -37,7 +37,7 @@
 
 (* theorem specifications *)
 
-val attrib = Parse.position (Parse.liberal_name -- Parse.!!! Args.parse) >> Args.src;
+val attrib = Parse.position Parse.liberal_name -- Parse.!!! Args.parse >> uncurry Args.src;
 val attribs = Parse.$$$ "[" |-- Parse.list attrib --| Parse.$$$ "]";
 val opt_attribs = Scan.optional attribs [];
 
diff -r 422024102d9d -r 8bedca4bd5a3 src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Mon Mar 10 15:30:29 2014 +0100
+++ b/src/Pure/ML/ml_context.ML	Mon Mar 10 16:30:07 2014 +0100
@@ -115,10 +115,8 @@
 fun check_antiq ctxt = #1 o Name_Space.check (Context.Proof ctxt) (get_antiqs ctxt);
 
 fun antiquotation src ctxt =
-  let
-    val ((xname, _), pos) = Args.dest_src src;
-    val (_, scan) = Name_Space.check (Context.Proof ctxt) (get_antiqs ctxt) (xname, pos);
-  in Args.context_syntax Markup.ML_antiquotationN scan src ctxt end;
+  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;
 
 
 (* parsing and evaluation *)
@@ -127,7 +125,7 @@
 
 val antiq =
   Parse.!!! (Parse.position Parse.xname -- Args.parse --| Scan.ahead Parse.eof)
-  >> (fn ((x, pos), y) => Args.src ((x, y), pos));
+  >> uncurry Args.src;
 
 val begin_env0 = ML_Lex.tokenize "structure Isabelle =\nstruct\n";
 
diff -r 422024102d9d -r 8bedca4bd5a3 src/Pure/Thy/term_style.ML
--- a/src/Pure/Thy/term_style.ML	Mon Mar 10 15:30:29 2014 +0100
+++ b/src/Pure/Thy/term_style.ML	Mon Mar 10 16:30:07 2014 +0100
@@ -42,10 +42,10 @@
 
 (* style parsing *)
 
-fun parse_single ctxt = Parse.position (Parse.xname -- Args.parse)
-  >> (fn x as ((name, _), _) => fst (Args.context_syntax "style"
+fun parse_single ctxt = Parse.position Parse.xname -- Args.parse
+  >> (fn ((name, pos), args) => fst (Args.context_syntax "style"
        (Scan.lift (the_style (Proof_Context.theory_of ctxt) name))
-         (Args.src x) ctxt |>> (fn f => f ctxt)));
+         (Args.src (name, pos) args) ctxt |>> (fn f => f ctxt)));
 
 val parse = Args.context :|-- (fn ctxt => Scan.lift
   (Args.parens (parse_single ctxt ::: Scan.repeat (Args.$$$ "," |-- parse_single ctxt))
diff -r 422024102d9d -r 8bedca4bd5a3 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Mon Mar 10 15:30:29 2014 +0100
+++ b/src/Pure/Thy/thy_output.ML	Mon Mar 10 16:30:07 2014 +0100
@@ -92,11 +92,8 @@
 fun check_option ctxt = #1 o Name_Space.check (Context.Proof ctxt) (#2 (get_antiquotations ctxt));
 
 fun command src state ctxt =
-  let
-    val ((xname, _), pos) = Args.dest_src src;
-    val (name, f) =
-      Name_Space.check (Context.Proof ctxt) (#1 (get_antiquotations ctxt)) (xname, pos);
-  in f src state ctxt end;
+  let val (src', f) = Args.check_src (Context.Proof ctxt) (#1 (get_antiquotations ctxt)) src
+  in f src' state ctxt end;
 
 fun option ((xname, pos), s) ctxt =
   let
@@ -155,7 +152,7 @@
 val antiq =
   Parse.!!!
     (Parse.position Parse.liberal_name -- properties -- Args.parse --| Scan.ahead Parse.eof)
-  >> (fn (((x, pos), y), z) => (y, Args.src ((x, z), pos)));
+  >> (fn ((name, props), args) => (props, Args.src name args));
 
 end;
 
@@ -615,12 +612,11 @@
 
 val _ = Theory.setup
   (antiquotation (Binding.name "lemma")
-    (Args.prop --
+    (Scan.lift (Scan.ahead Parse.not_eof) -- Args.prop --
       Scan.lift (Parse.position (Args.$$$ "by") -- Method.parse -- Scan.option Method.parse))
-    (fn {source, context = ctxt, ...} => fn (prop, (((_, by_pos), m1), m2)) =>
+    (fn {source, context = ctxt, ...} => fn ((prop_token, prop), (((_, by_pos), m1), m2)) =>
       let
-        val prop_src =
-          (case Args.dest_src source of ((a, arg :: _), pos) => Args.src ((a, [arg]), pos));
+        val prop_src = Args.src (Args.name_of_src source) [prop_token];
 
         val reports = (by_pos, Markup.keyword1) :: maps Method.reports_of (m1 :: the_list m2);
         val _ = Context_Position.reports ctxt reports;