--- 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
--- 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} ']'
;
--- 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
--- 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
--- 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;
--- 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 ||