# HG changeset patch
# User wenzelm
# Date 1397069912 -7200
# Node ID 90f17a04567d01131cf0759be3359280a5cf1b80
# Parent  7e0178c84994bf3807e1f2321fc7f60458c28b96
proper Args.name vs. Args.text as documented (in contrast to adhoc union in 75aaee32893d, which had to cope with more limited Args.T);

diff -r 7e0178c84994 -r 90f17a04567d src/HOL/ex/Cartouche_Examples.thy
--- a/src/HOL/ex/Cartouche_Examples.thy	Wed Apr 09 17:54:09 2014 +0200
+++ b/src/HOL/ex/Cartouche_Examples.thy	Wed Apr 09 20:58:32 2014 +0200
@@ -27,6 +27,9 @@
   txt \<open>Of course, this can be nested inside formal comments and
     antiquotations, e.g. like this @{thm \<open>x = y\<close>} or this @{thm sym
     [OF \<open>x = y\<close>]}.\<close>
+
+  have "x = y"
+    by (tactic \<open>rtac @{thm \<open>x = y\<close>} 1\<close>)  -- \<open>more cartouches involving ML\<close>
 end
 
 
diff -r 7e0178c84994 -r 90f17a04567d src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Wed Apr 09 17:54:09 2014 +0200
+++ b/src/Pure/Isar/args.ML	Wed Apr 09 20:58:32 2014 +0200
@@ -33,6 +33,8 @@
   val maybe: 'a parser -> 'a option parser
   val cartouche_inner_syntax: string parser
   val cartouche_source_position: Symbol_Pos.source parser
+  val text_source_position: Symbol_Pos.source parser
+  val text: string parser
   val name_inner_syntax: string parser
   val name_source_position: Symbol_Pos.source parser
   val name: string parser
@@ -151,7 +153,7 @@
   (Parse.short_ident || Parse.long_ident || Parse.sym_ident || Parse.term_var ||
     Parse.type_ident || Parse.type_var || Parse.number);
 
-val string = Parse.token (Parse.string || Parse.verbatim);
+val string = Parse.token Parse.string;
 val alt_string = Parse.token (Parse.alt_string || Parse.cartouche);
 val symbolic = Parse.token (Parse.keyword_with Token.ident_or_symbolic);
 
@@ -163,7 +165,6 @@
       else Scan.fail
     end);
 
-
 val named = ident || string;
 
 val add = $$$ "add";
@@ -183,6 +184,10 @@
 val cartouche_inner_syntax = cartouche >> Token.inner_syntax_of;
 val cartouche_source_position = cartouche >> Token.source_position_of;
 
+val text_token = named || Parse.token (Parse.verbatim || Parse.cartouche);
+val text_source_position = text_token >> Token.source_position_of;
+val text = text_token >> Token.content_of;
+
 val name_inner_syntax = named >> Token.inner_syntax_of;
 val name_source_position = named >> Token.source_position_of;
 
diff -r 7e0178c84994 -r 90f17a04567d src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Wed Apr 09 17:54:09 2014 +0200
+++ b/src/Pure/Isar/method.ML	Wed Apr 09 20:58:32 2014 +0200
@@ -513,9 +513,9 @@
   setup @{binding rotate_tac} (Args.goal_spec -- Scan.lift (Scan.optional Parse.int 1) >>
     (fn (quant, i) => K (SIMPLE_METHOD'' quant (rotate_tac i))))
       "rotate assumptions of goal" #>
-  setup @{binding tactic} (Scan.lift Args.name_source_position >> tactic)
+  setup @{binding tactic} (Scan.lift Args.text_source_position >> tactic)
     "ML tactic as proof method" #>
-  setup @{binding raw_tactic} (Scan.lift Args.name_source_position >> raw_tactic)
+  setup @{binding raw_tactic} (Scan.lift Args.text_source_position >> raw_tactic)
     "ML tactic as raw proof method");