# HG changeset patch
# User wenzelm
# Date 1395138429 -3600
# Node ID dd2df97b379b54388f4456af0c1a9a7ced7a6630
# Parent  1f9951be72b5e0ef84357928193f15f1f53b688b
tuned signature;

diff -r 1f9951be72b5 -r dd2df97b379b src/HOL/Tools/recdef.ML
--- a/src/HOL/Tools/recdef.ML	Tue Mar 18 11:13:38 2014 +0100
+++ b/src/HOL/Tools/recdef.ML	Tue Mar 18 11:27:09 2014 +0100
@@ -290,7 +290,7 @@
 
 val hints =
   @{keyword "("} |--
-    Parse.!!! (Parse.position @{keyword "hints"} -- Args.parse --| @{keyword ")"})
+    Parse.!!! (Parse.position @{keyword "hints"} -- Parse.args --| @{keyword ")"})
   >> uncurry Args.src;
 
 val recdef_decl =
diff -r 1f9951be72b5 -r dd2df97b379b src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Tue Mar 18 11:13:38 2014 +0100
+++ b/src/Pure/Isar/args.ML	Tue Mar 18 11:27:09 2014 +0100
@@ -61,8 +61,6 @@
   val type_name: {proper: bool, strict: bool} -> string context_parser
   val const: {proper: bool, strict: bool} -> string context_parser
   val goal_spec: ((int -> tactic) -> tactic) context_parser
-  val parse: Token.T list parser
-  val parse1: (string -> bool) -> Token.T list parser
   val attribs: (xstring * Position.T -> string) -> src list parser
   val opt_attribs: (xstring * Position.T -> string) -> src list parser
   val syntax_generic: 'a context_parser -> src -> Context.generic -> 'a * Context.generic
@@ -149,18 +147,16 @@
 
 (* basic *)
 
-fun token atom = Scan.ahead Parse.not_eof --| atom;
-
-val ident = token
+val ident = Parse.token
   (Parse.short_ident || Parse.long_ident || Parse.sym_ident || Parse.term_var ||
     Parse.type_ident || Parse.type_var || Parse.number);
 
-val string = token (Parse.string || Parse.verbatim);
-val alt_string = token Parse.alt_string;
-val symbolic = token (Parse.keyword_with Token.ident_or_symbolic);
+val string = Parse.token (Parse.string || Parse.verbatim);
+val alt_string = Parse.token Parse.alt_string;
+val symbolic = Parse.token (Parse.keyword_with Token.ident_or_symbolic);
 
 fun $$$ x =
-  (ident || token Parse.keyword) :|-- (fn tok =>
+  (ident || Parse.token Parse.keyword) :|-- (fn tok =>
     let val y = Token.content_of tok in
       if x = y
       then (Token.assign (SOME (Token.Literal Markup.quasi_keyword)) tok; Scan.succeed x)
@@ -183,7 +179,7 @@
 fun mode s = Scan.optional (parens ($$$ s) >> K true) false;
 fun maybe scan = $$$ "_" >> K NONE || scan >> SOME;
 
-val cartouche = token Parse.cartouche;
+val cartouche = Parse.token Parse.cartouche;
 val cartouche_inner_syntax = cartouche >> Token.inner_syntax_of;
 val cartouche_source_position = cartouche >> Token.source_position_of;
 
@@ -259,44 +255,13 @@
 fun goal_spec x = Scan.lift (Scan.optional goal (fn tac => tac 1)) x;
 
 
-(* arguments within outer syntax *)
-
-val argument_kinds =
- [Token.Ident, Token.LongIdent, Token.SymIdent, Token.Var, Token.TypeIdent, Token.TypeVar,
-  Token.Nat, Token.Float, Token.String, Token.AltString, Token.Cartouche, Token.Verbatim];
-
-fun parse_args is_symid =
-  let
-    fun argument blk =
-      Parse.group (fn () => "argument")
-        (Scan.one (fn tok =>
-          let val kind = Token.kind_of tok in
-            member (op =) argument_kinds kind orelse
-            Token.keyword_with is_symid tok orelse
-            (blk andalso Token.keyword_with (fn s => s = ",") tok)
-          end));
-
-    fun args blk x = Scan.optional (args1 blk) [] x
-    and args1 blk x =
-      ((Scan.repeat1
-        (Scan.repeat1 (argument blk) ||
-          argsp "(" ")" ||
-          argsp "[" "]")) >> flat) x
-    and argsp l r x =
-      (token (Parse.$$$ l) ::: Parse.!!! (args true @@@ (token (Parse.$$$ r) >> single))) x;
-  in (args, args1) end;
-
-val parse = #1 (parse_args Token.ident_or_symbolic) false;
-fun parse1 is_symid = #2 (parse_args is_symid) false;
-
-
 (* attributes *)
 
 fun attribs check =
   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 >> uncurry src;
+    val attrib = Parse.position attrib_name -- Parse.!!! Parse.args >> uncurry src;
   in $$$ "[" |-- Parse.!!! (Parse.list attrib --| $$$ "]") end;
 
 fun opt_attribs check = Scan.optional (attribs check) [];
diff -r 1f9951be72b5 -r dd2df97b379b src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Tue Mar 18 11:13:38 2014 +0100
+++ b/src/Pure/Isar/method.ML	Tue Mar 18 11:27:09 2014 +0100
@@ -458,7 +458,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 uncurry Args.src) ||
+ (Parse.position Parse.xname -- Parse.args1 is_symid_meth >> (Source o uncurry Args.src) ||
   meth3) x
 and meth1 x =
   (Parse.enum1_positions "," meth2
diff -r 1f9951be72b5 -r dd2df97b379b src/Pure/Isar/parse.ML
--- a/src/Pure/Isar/parse.ML	Tue Mar 18 11:13:38 2014 +0100
+++ b/src/Pure/Isar/parse.ML	Tue Mar 18 11:27:09 2014 +0100
@@ -15,6 +15,7 @@
   val triple2: 'a * ('b * 'c) -> 'a * 'b * 'c
   val triple_swap: ('a * 'b) * 'c -> ('a * 'c) * 'b
   val not_eof: Token.T parser
+  val token: 'a parser -> Token.T parser
   val position: 'a parser -> ('a * Position.T) parser
   val source_position: 'a parser -> Symbol_Pos.source parser
   val inner_syntax: 'a parser -> string parser
@@ -104,6 +105,8 @@
   val termp: (string * string list) parser
   val target: (xstring * Position.T) parser
   val opt_target: (xstring * Position.T) option parser
+  val args: Token.T list parser
+  val args1: (string -> bool) -> Token.T list parser
 end;
 
 structure Parse: PARSE =
@@ -168,6 +171,8 @@
 
 val not_eof = RESET_VALUE (Scan.one Token.not_eof);
 
+fun token atom = Scan.ahead not_eof --| atom;
+
 fun position scan = (Scan.ahead not_eof >> Token.pos_of) -- scan >> Library.swap;
 fun source_position atom = Scan.ahead atom |-- not_eof >> Token.source_position_of;
 fun inner_syntax atom = Scan.ahead atom |-- not_eof >> Token.inner_syntax_of;
@@ -393,6 +398,42 @@
 val target = ($$$ "(" -- $$$ "in") |-- !!! (position xname --| $$$ ")");
 val opt_target = Scan.option target;
 
+
+(* arguments within outer syntax *)
+
+local
+
+val argument_kinds =
+ [Token.Ident, Token.LongIdent, Token.SymIdent, Token.Var, Token.TypeIdent, Token.TypeVar,
+  Token.Nat, Token.Float, Token.String, Token.AltString, Token.Cartouche, Token.Verbatim];
+
+fun arguments is_symid =
+  let
+    fun argument blk =
+      group (fn () => "argument")
+        (Scan.one (fn tok =>
+          let val kind = Token.kind_of tok in
+            member (op =) argument_kinds kind orelse
+            Token.keyword_with is_symid tok orelse
+            (blk andalso Token.keyword_with (fn s => s = ",") tok)
+          end));
+
+    fun args blk x = Scan.optional (args1 blk) [] x
+    and args1 blk x =
+      ((Scan.repeat1
+        (Scan.repeat1 (argument blk) ||
+          argsp "(" ")" ||
+          argsp "[" "]")) >> flat) x
+    and argsp l r x = (token ($$$ l) ::: !!! (args true @@@ (token ($$$ r) >> single))) x;
+  in (args, args1) end;
+
+in
+
+val args = #1 (arguments Token.ident_or_symbolic) false;
+fun args1 is_symid = #2 (arguments is_symid) false;
+
+end;
+
 end;
 
 type 'a parser = 'a Parse.parser;
diff -r 1f9951be72b5 -r dd2df97b379b src/Pure/Isar/parse_spec.ML
--- a/src/Pure/Isar/parse_spec.ML	Tue Mar 18 11:13:38 2014 +0100
+++ b/src/Pure/Isar/parse_spec.ML	Tue Mar 18 11:27:09 2014 +0100
@@ -37,7 +37,7 @@
 
 (* theorem specifications *)
 
-val attrib = Parse.position Parse.liberal_name -- Parse.!!! Args.parse >> uncurry Args.src;
+val attrib = Parse.position Parse.liberal_name -- Parse.!!! Parse.args >> uncurry Args.src;
 val attribs = Parse.$$$ "[" |-- Parse.list attrib --| Parse.$$$ "]";
 val opt_attribs = Scan.optional attribs [];
 
diff -r 1f9951be72b5 -r dd2df97b379b src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Tue Mar 18 11:13:38 2014 +0100
+++ b/src/Pure/ML/ml_context.ML	Tue Mar 18 11:27:09 2014 +0100
@@ -91,7 +91,7 @@
 local
 
 val antiq =
-  Parse.!!! (Parse.position Parse.xname -- Args.parse --| Scan.ahead Parse.eof)
+  Parse.!!! (Parse.position Parse.xname -- Parse.args --| Scan.ahead Parse.eof)
   >> uncurry Args.src;
 
 val begin_env0 = ML_Lex.tokenize "structure Isabelle =\nstruct\n";
diff -r 1f9951be72b5 -r dd2df97b379b src/Pure/Thy/term_style.ML
--- a/src/Pure/Thy/term_style.ML	Tue Mar 18 11:13:38 2014 +0100
+++ b/src/Pure/Thy/term_style.ML	Tue Mar 18 11:27:09 2014 +0100
@@ -33,7 +33,7 @@
 (* style parsing *)
 
 fun parse_single ctxt =
-  Parse.position Parse.xname -- Args.parse >> (fn (name, args) =>
+  Parse.position Parse.xname -- Parse.args >> (fn (name, args) =>
     let
       val (src, parse) = Args.check_src ctxt (get_data ctxt) (Args.src name args);
       val (f, _) = Args.syntax (Scan.lift parse) src ctxt;
diff -r 1f9951be72b5 -r dd2df97b379b src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Tue Mar 18 11:13:38 2014 +0100
+++ b/src/Pure/Thy/thy_output.ML	Tue Mar 18 11:27:09 2014 +0100
@@ -151,7 +151,7 @@
 
 val antiq =
   Parse.!!!
-    (Parse.position Parse.liberal_name -- properties -- Args.parse --| Scan.ahead Parse.eof)
+    (Parse.position Parse.liberal_name -- properties -- Parse.args --| Scan.ahead Parse.eof)
   >> (fn ((name, props), args) => (props, Args.src name args));
 
 end;
diff -r 1f9951be72b5 -r dd2df97b379b src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Tue Mar 18 11:13:38 2014 +0100
+++ b/src/Tools/Code/code_target.ML	Tue Mar 18 11:27:09 2014 +0100
@@ -646,7 +646,7 @@
   Parse.enum1 "|" (Parse.group (fn () => "code symbol pragma")
     (parse_symbol_pragma parse_const parse_tyco parse_class parse_classrel parse_inst parse_module));
 
-val code_expr_argsP = Scan.optional (@{keyword "("} |-- Args.parse --| @{keyword ")"}) [];
+val code_expr_argsP = Scan.optional (@{keyword "("} |-- Parse.args --| @{keyword ")"}) [];
 
 fun code_expr_inP all_public raw_cs =
   Scan.repeat (@{keyword "in"} |-- Parse.!!! (Parse.name