# HG changeset patch
# User boehmes
# Date 1390168920 -3600
# Node ID de68c9c3e4549839d7f500d002e444e26de6f1d3
# Parent  327eafb594ba1524a4b8ff1c63a08d888e90c566# Parent  ce34a293438651dd8d618e28f28bec7c04cd88e7
merged

diff -r 327eafb594ba -r de68c9c3e454 etc/symbols
--- a/etc/symbols	Sun Jan 19 22:38:17 2014 +0100
+++ b/etc/symbols	Sun Jan 19 23:02:00 2014 +0100
@@ -348,8 +348,8 @@
 \<hungarumlaut>         code: 0x0002dd
 \<some>                 code: 0x0003f5
 \<newline>              code: 0x0023ce
-\<open>                 code: 0x002039  abbrev: <<  font: IsabelleText
-\<close>                code: 0x00203a  abbrev: >>  font: IsabelleText
+\<open>                 code: 0x002039  group: punctuation  font: IsabelleText  abbrev: <<
+\<close>                code: 0x00203a  group: punctuation  font: IsabelleText  abbrev: >>
 \<^sub>                 code: 0x0021e9  group: control  font: IsabelleText
 \<^sup>                 code: 0x0021e7  group: control  font: IsabelleText
 \<^bold>                code: 0x002759  group: control  font: IsabelleText
diff -r 327eafb594ba -r de68c9c3e454 src/Doc/IsarRef/Outer_Syntax.thy
--- a/src/Doc/IsarRef/Outer_Syntax.thy	Sun Jan 19 22:38:17 2014 +0100
+++ b/src/Doc/IsarRef/Outer_Syntax.thy	Sun Jan 19 23:02:00 2014 +0100
@@ -401,7 +401,7 @@
   @{rail "
     @{syntax_def atom}: @{syntax nameref} | @{syntax typefree} |
       @{syntax typevar} | @{syntax var} | @{syntax nat} | @{syntax float} |
-      @{syntax keyword}
+      @{syntax keyword} | @{syntax cartouche}
     ;
     arg: @{syntax atom} | '(' @{syntax args} ')' | '[' @{syntax args} ']'
     ;
diff -r 327eafb594ba -r de68c9c3e454 src/HOL/ex/Cartouche_Examples.thy
--- a/src/HOL/ex/Cartouche_Examples.thy	Sun Jan 19 22:38:17 2014 +0100
+++ b/src/HOL/ex/Cartouche_Examples.thy	Sun Jan 19 23:02:00 2014 +0100
@@ -58,4 +58,67 @@
 term "STR \<open>abc\<close>"
 lemma "STR \<open>abc\<close> @ STR \<open>xyz\<close> = STR \<open>abcxyz\<close>" by simp
 
+
+subsection {* Proof method syntax *}
+
+ML {*
+structure ML_Tactic:
+sig
+  val set: (Proof.context -> tactic) -> Proof.context -> Proof.context
+  val ml_tactic: string * Position.T -> Proof.context -> tactic
+end =
+struct
+  structure Data = Proof_Data(type T = Proof.context -> tactic fun init _ = K no_tac);
+
+  val set = Data.put;
+
+  fun ml_tactic (txt, pos) ctxt =
+    let
+      val ctxt' = ctxt |> Context.proof_map
+        (ML_Context.expression pos
+          "fun tactic (ctxt : Proof.context) : tactic"
+          "Context.map_proof (ML_Tactic.set tactic)" (ML_Lex.read pos txt));
+    in Data.get ctxt' ctxt end;
+end;
+*}
+
+
+subsection {* Explicit version: method with cartouche argument *}
+
+method_setup ml_tactic = {*
+  Scan.lift Args.cartouche_source_position
+    >> (fn arg => fn ctxt => SIMPLE_METHOD (ML_Tactic.ml_tactic arg ctxt))
+*}
+
+lemma "A \<and> B \<longrightarrow> B \<and> A"
+  apply (ml_tactic \<open>rtac @{thm impI} 1\<close>)
+  apply (ml_tactic \<open>etac @{thm conjE} 1\<close>)
+  apply (ml_tactic \<open>rtac @{thm conjI} 1\<close>)
+  apply (ml_tactic \<open>ALLGOALS atac\<close>)
+  done
+
+lemma "A \<and> B \<longrightarrow> B \<and> A" by (ml_tactic \<open>blast_tac ctxt 1\<close>)
+
+ML {* @{lemma "A \<and> B \<longrightarrow> B \<and> A" by (ml_tactic \<open>blast_tac ctxt 1\<close>)} *}
+
+text {* @{ML "@{lemma \"A \<and> B \<longrightarrow> B \<and> A\" by (ml_tactic \<open>blast_tac ctxt 1\<close>)}"} *}
+
+
+subsection {* Implicit version: method with special name "cartouche" (dynamic!) *}
+
+method_setup "cartouche" = {*
+  Scan.lift Args.cartouche_source_position
+    >> (fn arg => fn ctxt => SIMPLE_METHOD (ML_Tactic.ml_tactic arg ctxt))
+*}
+
+lemma "A \<and> B \<longrightarrow> B \<and> A"
+  apply \<open>rtac @{thm impI} 1\<close>
+  apply \<open>etac @{thm conjE} 1\<close>
+  apply \<open>rtac @{thm conjI} 1\<close>
+  apply \<open>ALLGOALS atac\<close>
+  done
+
+lemma "A \<and> B \<longrightarrow> B \<and> A"
+  by (\<open>rtac @{thm impI} 1\<close>, \<open>etac @{thm conjE} 1\<close>, \<open>rtac @{thm conjI} 1\<close>, \<open>atac 1\<close>+)
+
 end
diff -r 327eafb594ba -r de68c9c3e454 src/Pure/General/antiquote.ML
--- a/src/Pure/General/antiquote.ML	Sun Jan 19 22:38:17 2014 +0100
+++ b/src/Pure/General/antiquote.ML	Sun Jan 19 23:02:00 2014 +0100
@@ -50,6 +50,7 @@
 
 val scan_ant =
   Scan.trace (Symbol_Pos.scan_string_qq err_prefix || Symbol_Pos.scan_string_bq err_prefix) >> #2 ||
+  Scan.trace (Symbol_Pos.scan_cartouche (fn s => Symbol_Pos.!!! (fn () => err_prefix ^ s))) >> #2 ||
   Scan.one (fn (s, _) => s <> "}" andalso Symbol.is_regular s) >> single;
 
 in
diff -r 327eafb594ba -r de68c9c3e454 src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Sun Jan 19 22:38:17 2014 +0100
+++ b/src/Pure/Isar/args.ML	Sun Jan 19 23:02:00 2014 +0100
@@ -29,6 +29,8 @@
   val bracks: 'a parser -> 'a parser
   val mode: string -> bool parser
   val maybe: 'a parser -> 'a option parser
+  val cartouche_source: string parser
+  val cartouche_source_position: (Symbol_Pos.text * Position.T) parser
   val name_source: string parser
   val name_source_position: (Symbol_Pos.text * Position.T) parser
   val name: string parser
@@ -148,6 +150,10 @@
 fun mode s = Scan.optional (parens ($$$ s) >> K true) false;
 fun maybe scan = $$$ "_" >> K NONE || scan >> SOME;
 
+val cartouche = token Parse.cartouche;
+val cartouche_source = cartouche >> Token.source_of;
+val cartouche_source_position = cartouche >> Token.source_position_of;
+
 val name_source = named >> Token.source_of;
 val name_source_position = named >> Token.source_position_of;
 
diff -r 327eafb594ba -r de68c9c3e454 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Sun Jan 19 22:38:17 2014 +0100
+++ b/src/Pure/Isar/method.ML	Sun Jan 19 23:02:00 2014 +0100
@@ -406,6 +406,9 @@
 
 fun meth4 x =
  (Parse.position (Parse.xname >> rpair []) >> (Source o Args.src) ||
+  (* FIXME implicit "cartouche" method (experimental, undocumented) *)
+  Scan.ahead Parse.cartouche |-- Parse.not_eof >> (fn tok =>
+    Source (Args.src (("cartouche", [tok]), Token.position_of tok))) ||
   Parse.$$$ "(" |-- Parse.!!! (meth0 --| Parse.$$$ ")")) x
 and meth3 x =
  (meth4 --| Parse.$$$ "?" >> Try ||