--- a/NEWS Mon May 23 22:43:22 2016 +0200
+++ b/NEWS Tue May 24 11:39:26 2016 +0200
@@ -9,6 +9,10 @@
*** General ***
+* Embedded content (e.g. the inner syntax of types, terms, props) may be
+delimited uniformly via cartouches. This works better than old-fashioned
+quotes when sub-languages are nested.
+
* Type-inference improves sorts of newly introduced type variables for
the object-logic, using its base sort (i.e. HOL.type for Isabelle/HOL).
Thus terms like "f x" or "\<And>x. P x" without any further syntactic context
--- a/src/CCL/CCL.thy Mon May 23 22:43:22 2016 +0200
+++ b/src/CCL/CCL.thy Tue May 24 11:39:26 2016 +0200
@@ -474,7 +474,7 @@
done
method_setup eq_coinduct3 = \<open>
- Scan.lift Args.name_inner_syntax >> (fn s => fn ctxt =>
+ Scan.lift Args.embedded_inner_syntax >> (fn s => fn ctxt =>
SIMPLE_METHOD'
(Rule_Insts.res_inst_tac ctxt [((("R", 0), Position.none), s)] [] @{thm eq_coinduct3}))
\<close>
--- a/src/CCL/Wfd.thy Mon May 23 22:43:22 2016 +0200
+++ b/src/CCL/Wfd.thy Tue May 24 11:39:26 2016 +0200
@@ -47,7 +47,7 @@
done
method_setup wfd_strengthen = \<open>
- Scan.lift Args.name_inner_syntax >> (fn s => fn ctxt =>
+ Scan.lift Args.embedded_inner_syntax >> (fn s => fn ctxt =>
SIMPLE_METHOD' (fn i =>
Rule_Insts.res_inst_tac ctxt [((("Q", 0), Position.none), s)] [] @{thm wfd_strengthen_lemma} i
THEN assume_tac ctxt (i + 1)))
--- a/src/CTT/CTT.thy Mon May 23 22:43:22 2016 +0200
+++ b/src/CTT/CTT.thy Tue May 24 11:39:26 2016 +0200
@@ -449,7 +449,7 @@
method_setup eqintr = \<open>Scan.succeed (SIMPLE_METHOD o eqintr_tac)\<close>
method_setup NE = \<open>
- Scan.lift Args.name_inner_syntax >> (fn s => fn ctxt => SIMPLE_METHOD' (NE_tac ctxt s))
+ Scan.lift Args.embedded_inner_syntax >> (fn s => fn ctxt => SIMPLE_METHOD' (NE_tac ctxt s))
\<close>
method_setup pc = \<open>Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD' (pc_tac ctxt ths))\<close>
method_setup add_mp = \<open>Scan.succeed (SIMPLE_METHOD' o add_mp_tac)\<close>
--- a/src/Doc/Isar_Ref/Document_Preparation.thy Mon May 23 22:43:22 2016 +0200
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy Tue May 24 11:39:26 2016 +0200
@@ -177,8 +177,8 @@
@@{antiquotation const} options @{syntax term} |
@@{antiquotation abbrev} options @{syntax term} |
@@{antiquotation typ} options @{syntax type} |
- @@{antiquotation type} options @{syntax name} |
- @@{antiquotation class} options @{syntax name} |
+ @@{antiquotation type} options @{syntax embedded} |
+ @@{antiquotation class} options @{syntax embedded} |
(@@{antiquotation command} | @@{antiquotation method} | @@{antiquotation attribute})
options @{syntax name}
;
@@ -197,7 +197,7 @@
@@{antiquotation verbatim} options @{syntax text} |
@@{antiquotation "file"} options @{syntax name} |
@@{antiquotation file_unchecked} options @{syntax name} |
- @@{antiquotation url} options @{syntax name} |
+ @@{antiquotation url} options @{syntax embedded} |
@@{antiquotation cite} options @{syntax cartouche}? (@{syntax name} + @'and')
;
styles: '(' (style + ',') ')'
--- a/src/Doc/Isar_Ref/Outer_Syntax.thy Mon May 23 22:43:22 2016 +0200
+++ b/src/Doc/Isar_Ref/Outer_Syntax.thy Tue May 24 11:39:26 2016 +0200
@@ -184,7 +184,7 @@
@{rail \<open>
@{syntax_def name}: @{syntax ident} | @{syntax longident} |
- @{syntax symident} | @{syntax string} | @{syntax nat}
+ @{syntax symident} | @{syntax nat} | @{syntax string}
;
@{syntax_def par_name}: '(' @{syntax name} ')'
\<close>}
@@ -209,6 +209,24 @@
\<close>
+subsection \<open>Embedded content\<close>
+
+text \<open>
+ Entity @{syntax embedded} refers to content of other languages: cartouches
+ allow arbitrary nesting of sub-languages that respect the recursive
+ balancing of cartouche delimiters. Quoted strings are possible as well, but
+ require escaped quotes when nested. As a shortcut, tokens that appear as
+ plain identifiers in the outer language may be used as inner language
+ content without delimiters.
+
+ @{rail \<open>
+ @{syntax_def embedded}: @{syntax cartouche} | @{syntax string} |
+ @{syntax ident} | @{syntax longident} | @{syntax symident} |
+ @{syntax nat}
+ \<close>}
+\<close>
+
+
subsection \<open>Comments \label{sec:comments}\<close>
text \<open>
@@ -260,10 +278,10 @@
as \<^verbatim>\<open>=\<close> or \<^verbatim>\<open>+\<close>).
@{rail \<open>
- @{syntax_def type}: @{syntax name} | @{syntax typefree} |
+ @{syntax_def type}: @{syntax embedded} | @{syntax typefree} |
@{syntax typevar}
;
- @{syntax_def term}: @{syntax name} | @{syntax var}
+ @{syntax_def term}: @{syntax embedded} | @{syntax var}
;
@{syntax_def prop}: @{syntax term}
\<close>}
--- a/src/Doc/Prog_Prove/LaTeXsugar.thy Mon May 23 22:43:22 2016 +0200
+++ b/src/Doc/Prog_Prove/LaTeXsugar.thy Tue May 24 11:39:26 2016 +0200
@@ -52,7 +52,7 @@
end
in
Thy_Output.antiquotation @{binding "const_typ"}
- (Scan.lift Args.name_inner_syntax)
+ (Scan.lift Args.embedded_inner_syntax)
(fn {source = src, context = ctxt, ...} => fn arg =>
Thy_Output.output ctxt
(Thy_Output.maybe_pretty_source pretty ctxt src [arg]))
--- a/src/FOL/FOL.thy Mon May 23 22:43:22 2016 +0200
+++ b/src/FOL/FOL.thy Tue May 24 11:39:26 2016 +0200
@@ -72,7 +72,7 @@
\<close>
method_setup case_tac = \<open>
- Args.goal_spec -- Scan.lift (Args.name_inner_syntax -- Parse.for_fixes) >>
+ Args.goal_spec -- Scan.lift (Args.embedded_inner_syntax -- Parse.for_fixes) >>
(fn (quant, (s, fixes)) => fn ctxt => SIMPLE_METHOD'' quant (case_tac ctxt s fixes))
\<close> "case_tac emulation (dynamic instantiation!)"
--- a/src/HOL/Eisbach/parse_tools.ML Mon May 23 22:43:22 2016 +0200
+++ b/src/HOL/Eisbach/parse_tools.ML Tue May 24 11:39:26 2016 +0200
@@ -34,7 +34,7 @@
(fn ((_, SOME t), _) => Real_Val t
| ((tok, NONE), v) => Parse_Val (v, fn t => ignore (Token.assign (SOME (Token.Term t)) tok)));
-val name_term = parse_term_val Args.name_inner_syntax;
+val name_term = parse_term_val Args.embedded_inner_syntax;
fun is_real_val (Real_Val _) = true
| is_real_val _ = false;
--- a/src/HOL/HOLCF/IOA/CompoScheds.thy Mon May 23 22:43:22 2016 +0200
+++ b/src/HOL/HOLCF/IOA/CompoScheds.thy Tue May 24 11:39:26 2016 +0200
@@ -289,7 +289,7 @@
\<close>
method_setup mkex_induct = \<open>
- Scan.lift (Args.name -- Args.name -- Args.name)
+ Scan.lift (Args.embedded -- Args.embedded -- Args.embedded)
>> (fn ((sch, exA), exB) => fn ctxt =>
SIMPLE_METHOD' (mkex_induct_tac ctxt sch exA exB))
\<close>
--- a/src/HOL/HOLCF/IOA/Sequence.thy Mon May 23 22:43:22 2016 +0200
+++ b/src/HOL/HOLCF/IOA/Sequence.thy Tue May 24 11:39:26 2016 +0200
@@ -996,13 +996,13 @@
\<close>
method_setup Seq_case =
- \<open>Scan.lift Args.name >> (fn s => fn ctxt => SIMPLE_METHOD' (Seq_case_tac ctxt s))\<close>
+ \<open>Scan.lift Args.embedded >> (fn s => fn ctxt => SIMPLE_METHOD' (Seq_case_tac ctxt s))\<close>
method_setup Seq_case_simp =
- \<open>Scan.lift Args.name >> (fn s => fn ctxt => SIMPLE_METHOD' (Seq_case_simp_tac ctxt s))\<close>
+ \<open>Scan.lift Args.embedded >> (fn s => fn ctxt => SIMPLE_METHOD' (Seq_case_simp_tac ctxt s))\<close>
method_setup Seq_induct =
- \<open>Scan.lift Args.name --
+ \<open>Scan.lift Args.embedded --
Scan.optional ((Scan.lift (Args.$$$ "simp" -- Args.colon) |-- Attrib.thms)) []
>> (fn (s, rws) => fn ctxt => SIMPLE_METHOD' (Seq_induct_tac ctxt s rws))\<close>
@@ -1010,10 +1010,10 @@
\<open>Scan.succeed (SIMPLE_METHOD' o Seq_Finite_induct_tac)\<close>
method_setup pair =
- \<open>Scan.lift Args.name >> (fn s => fn ctxt => SIMPLE_METHOD' (pair_tac ctxt s))\<close>
+ \<open>Scan.lift Args.embedded >> (fn s => fn ctxt => SIMPLE_METHOD' (pair_tac ctxt s))\<close>
method_setup pair_induct =
- \<open>Scan.lift Args.name --
+ \<open>Scan.lift Args.embedded --
Scan.optional ((Scan.lift (Args.$$$ "simp" -- Args.colon) |-- Attrib.thms)) []
>> (fn (s, rws) => fn ctxt => SIMPLE_METHOD' (pair_induct_tac ctxt s rws))\<close>
--- a/src/HOL/Library/LaTeXsugar.thy Mon May 23 22:43:22 2016 +0200
+++ b/src/HOL/Library/LaTeXsugar.thy Tue May 24 11:39:26 2016 +0200
@@ -105,7 +105,7 @@
end
in
Thy_Output.antiquotation @{binding "const_typ"}
- (Scan.lift Args.name_inner_syntax)
+ (Scan.lift Args.embedded_inner_syntax)
(fn {source = src, context = ctxt, ...} => fn arg =>
Thy_Output.output ctxt
(Thy_Output.maybe_pretty_source pretty ctxt src [arg]))
--- a/src/HOL/Tools/Lifting/lifting_setup.ML Mon May 23 22:43:22 2016 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML Tue May 24 11:39:26 2016 +0200
@@ -1018,7 +1018,7 @@
val _ =
Outer_Syntax.local_theory @{command_keyword lifting_forget}
"unsetup Lifting and Transfer for the given lifting bundle"
- (Parse.position Parse.name >> (lifting_forget_cmd))
+ (Parse.position Parse.name >> lifting_forget_cmd)
(* lifting_update *)
--- a/src/HOL/Tools/functor.ML Mon May 23 22:43:22 2016 +0200
+++ b/src/HOL/Tools/functor.ML Tue May 24 11:39:26 2016 +0200
@@ -277,7 +277,6 @@
val _ =
Outer_Syntax.local_theory_to_proof @{command_keyword functor}
"register operations managing the functorial structure of a type"
- (Scan.option (Parse.name --| @{keyword ":"}) -- Parse.term
- >> (fn (prfx, t) => functor_cmd prfx t));
+ (Scan.option (Parse.name --| @{keyword ":"}) -- Parse.term >> uncurry functor_cmd);
end;
--- a/src/HOL/UNITY/UNITY_Main.thy Mon May 23 22:43:22 2016 +0200
+++ b/src/HOL/UNITY/UNITY_Main.thy Tue May 24 11:39:26 2016 +0200
@@ -16,7 +16,7 @@
"for proving safety properties"
method_setup ensures_tac = {*
- Args.goal_spec -- Scan.lift Args.name_inner_syntax >>
+ Args.goal_spec -- Scan.lift Args.embedded_inner_syntax >>
(fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (ensures_tac ctxt s))
*} "for proving progress properties"
--- a/src/HOL/ex/Cartouche_Examples.thy Mon May 23 22:43:22 2016 +0200
+++ b/src/HOL/ex/Cartouche_Examples.thy Tue May 24 11:39:26 2016 +0200
@@ -7,7 +7,7 @@
theory Cartouche_Examples
imports Main
keywords
- "cartouche" "term_cartouche" :: diag and
+ "cartouche" :: diag and
"text_cartouche" :: thy_decl
begin
@@ -19,21 +19,23 @@
notepad
begin
- txt \<open>Moreover, cartouches work as additional syntax in the
- \<open>altstring\<close> category, for literal fact references. For example:\<close>
+ txt \<open>Cartouches work as additional syntax for embedded language tokens
+ (types, terms, props) and as a replacement for the \<open>altstring\<close> category
+ (for literal fact references). For example:\<close>
fix x y :: 'a
- assume "x = y"
+ assume \<open>x = y\<close>
note \<open>x = y\<close>
- have "x = y" by (rule \<open>x = y\<close>)
- from \<open>x = y\<close> have "x = y" .
+ have \<open>x = y\<close> by (rule \<open>x = y\<close>)
+ from \<open>x = y\<close> have \<open>x = y\<close> .
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>resolve_tac @{context} @{thms \<open>x = y\<close>} 1\<close>) \<comment> \<open>more cartouches involving ML\<close>
+ have \<open>x = y\<close>
+ by (tactic \<open>resolve_tac @{context} @{thms \<open>x = y\<close>} 1\<close>)
+ \<comment> \<open>more cartouches involving ML\<close>
end
@@ -78,92 +80,55 @@
end;
\<close>
-syntax "_cartouche_string" :: "cartouche_position \<Rightarrow> string" ("_")
+syntax "_cartouche_string" :: \<open>cartouche_position \<Rightarrow> string\<close> ("_")
parse_translation \<open>
[(@{syntax_const "_cartouche_string"},
K (string_tr (Symbol_Pos.cartouche_content o Symbol_Pos.explode)))]
\<close>
-term "\<open>\<close>"
-term "\<open>abc\<close>"
-term "\<open>abc\<close> @ \<open>xyz\<close>"
-term "\<open>\<newline>\<close>"
-term "\<open>\001\010\100\<close>"
+term \<open>\<open>\<close>\<close>
+term \<open>\<open>abc\<close>\<close>
+term \<open>\<open>abc\<close> @ \<open>xyz\<close>\<close>
+term \<open>\<open>\<newline>\<close>\<close>
subsection \<open>Alternate outer and inner syntax: string literals\<close>
subsubsection \<open>Nested quotes\<close>
-syntax "_string_string" :: "string_position \<Rightarrow> string" ("_")
+syntax "_string_string" :: \<open>string_position \<Rightarrow> string\<close> ("_")
parse_translation \<open>
[(@{syntax_const "_string_string"}, K (string_tr Lexicon.explode_string))]
\<close>
-term "\"\""
-term "\"abc\""
-term "\"abc\" @ \"xyz\""
-term "\"\<newline>\""
-term "\"\001\010\100\""
-
-
-subsubsection \<open>Term cartouche and regular quotes\<close>
-
-ML \<open>
- Outer_Syntax.command @{command_keyword term_cartouche} ""
- (Parse.inner_syntax Parse.cartouche >> (fn s =>
- Toplevel.keep (fn state =>
- let
- val ctxt = Toplevel.context_of state;
- val t = Syntax.read_term ctxt s;
- in writeln (Syntax.string_of_term ctxt t) end)))
-\<close>
-
-term_cartouche \<open>""\<close>
-term_cartouche \<open>"abc"\<close>
-term_cartouche \<open>"abc" @ "xyz"\<close>
-term_cartouche \<open>"\<newline>"\<close>
-term_cartouche \<open>"\001\010\100"\<close>
+term \<open>""\<close>
+term \<open>"abc"\<close>
+term \<open>"abc" @ "xyz"\<close>
+term \<open>"\<newline>"\<close>
+term \<open>"\001\010\100"\<close>
subsubsection \<open>Further nesting: antiquotations\<close>
-setup \<comment> "ML antiquotation"
-\<open>
- ML_Antiquotation.inline @{binding term_cartouche}
- (Args.context -- Scan.lift (Parse.inner_syntax Parse.cartouche) >>
- (fn (ctxt, s) => ML_Syntax.atomic (ML_Syntax.print_term (Syntax.read_term ctxt s))))
-\<close>
-
-setup \<comment> "document antiquotation"
-\<open>
- Thy_Output.antiquotation @{binding ML_cartouche}
- (Scan.lift Args.cartouche_input) (fn {context, ...} => fn source =>
- let
- val toks = ML_Lex.read "fn _ => (" @ ML_Lex.read_source false source @ ML_Lex.read ");";
- val _ = ML_Context.eval_in (SOME context) ML_Compiler.flags (Input.pos_of source) toks;
- in "" end);
-\<close>
-
ML \<open>
- @{term_cartouche \<open>""\<close>};
- @{term_cartouche \<open>"abc"\<close>};
- @{term_cartouche \<open>"abc" @ "xyz"\<close>};
- @{term_cartouche \<open>"\<newline>"\<close>};
- @{term_cartouche \<open>"\001\010\100"\<close>};
+ @{term \<open>""\<close>};
+ @{term \<open>"abc"\<close>};
+ @{term \<open>"abc" @ "xyz"\<close>};
+ @{term \<open>"\<newline>"\<close>};
+ @{term \<open>"\001\010\100"\<close>};
\<close>
text \<open>
- @{ML_cartouche
+ @{ML
\<open>
(
- @{term_cartouche \<open>""\<close>};
- @{term_cartouche \<open>"abc"\<close>};
- @{term_cartouche \<open>"abc" @ "xyz"\<close>};
- @{term_cartouche \<open>"\<newline>"\<close>};
- @{term_cartouche \<open>"\001\010\100"\<close>}
+ @{term \<open>""\<close>};
+ @{term \<open>"abc"\<close>};
+ @{term \<open>"abc" @ "xyz"\<close>};
+ @{term \<open>"\<newline>"\<close>};
+ @{term \<open>"\001\010\100"\<close>}
)
\<close>
}
@@ -181,14 +146,14 @@
text_cartouche
\<open>
- @{ML_cartouche
+ @{ML
\<open>
(
- @{term_cartouche \<open>""\<close>};
- @{term_cartouche \<open>"abc"\<close>};
- @{term_cartouche \<open>"abc" @ "xyz"\<close>};
- @{term_cartouche \<open>"\<newline>"\<close>};
- @{term_cartouche \<open>"\001\010\100"\<close>}
+ @{term \<open>""\<close>};
+ @{term \<open>"abc"\<close>};
+ @{term \<open>"abc" @ "xyz"\<close>};
+ @{term \<open>"\<newline>"\<close>};
+ @{term \<open>"\001\010\100"\<close>}
)
\<close>
}
@@ -226,18 +191,18 @@
>> (fn arg => fn ctxt => SIMPLE_METHOD (ML_Tactic.ml_tactic arg ctxt))
\<close>
-lemma "A \<and> B \<longrightarrow> B \<and> A"
+lemma \<open>A \<and> B \<longrightarrow> B \<and> A\<close>
apply (ml_tactic \<open>resolve_tac @{context} @{thms impI} 1\<close>)
apply (ml_tactic \<open>eresolve_tac @{context} @{thms conjE} 1\<close>)
apply (ml_tactic \<open>resolve_tac @{context} @{thms conjI} 1\<close>)
apply (ml_tactic \<open>ALLGOALS (assume_tac @{context})\<close>)
done
-lemma "A \<and> B \<longrightarrow> B \<and> A" by (ml_tactic \<open>blast_tac ctxt 1\<close>)
+lemma \<open>A \<and> B \<longrightarrow> B \<and> A\<close> by (ml_tactic \<open>blast_tac ctxt 1\<close>)
-ML \<open>@{lemma "A \<and> B \<longrightarrow> B \<and> A" by (ml_tactic \<open>blast_tac ctxt 1\<close>)}\<close>
+ML \<open>@{lemma \<open>A \<and> B \<longrightarrow> B \<and> A\<close> by (ml_tactic \<open>blast_tac ctxt 1\<close>)}\<close>
-text \<open>@{ML "@{lemma \"A \<and> B \<longrightarrow> B \<and> A\" by (ml_tactic \<open>blast_tac ctxt 1\<close>)}"}\<close>
+text \<open>@{ML \<open>@{lemma \<open>A \<and> B \<longrightarrow> B \<and> A\<close> by (ml_tactic \<open>blast_tac ctxt 1\<close>)}\<close>}\<close>
subsubsection \<open>Implicit version: method with special name "cartouche" (dynamic!)\<close>
@@ -247,14 +212,14 @@
>> (fn arg => fn ctxt => SIMPLE_METHOD (ML_Tactic.ml_tactic arg ctxt))
\<close>
-lemma "A \<and> B \<longrightarrow> B \<and> A"
+lemma \<open>A \<and> B \<longrightarrow> B \<and> A\<close>
apply \<open>resolve_tac @{context} @{thms impI} 1\<close>
apply \<open>eresolve_tac @{context} @{thms conjE} 1\<close>
apply \<open>resolve_tac @{context} @{thms conjI} 1\<close>
apply \<open>ALLGOALS (assume_tac @{context})\<close>
done
-lemma "A \<and> B \<longrightarrow> B \<and> A"
+lemma \<open>A \<and> B \<longrightarrow> B \<and> A\<close>
by (\<open>resolve_tac @{context} @{thms impI} 1\<close>,
\<open>eresolve_tac @{context} @{thms conjE} 1\<close>,
\<open>resolve_tac @{context} @{thms conjI} 1\<close>,
--- a/src/LCF/LCF.thy Mon May 23 22:43:22 2016 +0200
+++ b/src/LCF/LCF.thy Tue May 24 11:39:26 2016 +0200
@@ -319,7 +319,7 @@
adm_not_eq_tr adm_conj adm_disj adm_imp adm_all
method_setup induct = \<open>
- Scan.lift Args.name_inner_syntax >> (fn v => fn ctxt =>
+ Scan.lift Args.embedded_inner_syntax >> (fn v => fn ctxt =>
SIMPLE_METHOD' (fn i =>
Rule_Insts.res_inst_tac ctxt [((("f", 0), Position.none), v)] [] @{thm induct} i THEN
REPEAT (resolve_tac ctxt @{thms adm_lemmas} i)))
--- a/src/Pure/Isar/args.ML Mon May 23 22:43:22 2016 +0200
+++ b/src/Pure/Isar/args.ML Tue May 24 11:39:26 2016 +0200
@@ -23,12 +23,14 @@
val mode: string -> bool parser
val maybe: 'a parser -> 'a option parser
val name_token: Token.T parser
- val name_inner_syntax: string parser
- val name_input: Input.source parser
val name: string parser
val cartouche_inner_syntax: string parser
val cartouche_input: Input.source parser
val text_token: Token.T parser
+ val embedded_token: Token.T parser
+ val embedded_inner_syntax: string parser
+ val embedded_input: Input.source parser
+ val embedded: string parser
val text_input: Input.source parser
val text: string parser
val binding: binding parser
@@ -104,15 +106,18 @@
fun maybe scan = $$$ "_" >> K NONE || scan >> SOME;
val name_token = ident || string;
-val name_inner_syntax = name_token >> Token.inner_syntax_of;
-val name_input = name_token >> Token.input_of;
val name = name_token >> Token.content_of;
val cartouche = Parse.token Parse.cartouche;
val cartouche_inner_syntax = cartouche >> Token.inner_syntax_of;
val cartouche_input = cartouche >> Token.input_of;
-val text_token = name_token || Parse.token (Parse.verbatim || Parse.cartouche);
+val embedded_token = ident || string || cartouche;
+val embedded_inner_syntax = embedded_token >> Token.inner_syntax_of;
+val embedded_input = embedded_token >> Token.input_of;
+val embedded = embedded_token >> Token.content_of;
+
+val text_token = embedded_token || Parse.token Parse.verbatim;
val text_input = text_token >> Token.input_of;
val text = text_token >> Token.content_of;
@@ -120,8 +125,9 @@
val alt_name = alt_string >> Token.content_of;
val liberal_name = (symbolic >> Token.content_of) || name;
-val var = (ident >> Token.content_of) :|-- (fn x =>
- (case Lexicon.read_variable x of SOME v => Scan.succeed v | NONE => Scan.fail));
+val var =
+ (ident >> Token.content_of) :|-- (fn x =>
+ (case Lexicon.read_variable x of SOME v => Scan.succeed v | NONE => Scan.fail));
(* values *)
@@ -141,10 +147,10 @@
internal_source || name_token >> Token.evaluate Token.Source read;
fun named_typ read =
- internal_typ || name_token >> Token.evaluate Token.Typ (read o Token.inner_syntax_of);
+ internal_typ || embedded_token >> Token.evaluate Token.Typ (read o Token.inner_syntax_of);
fun named_term read =
- internal_term || name_token >> Token.evaluate Token.Term (read o Token.inner_syntax_of);
+ internal_term || embedded_token >> Token.evaluate Token.Term (read o Token.inner_syntax_of);
fun named_fact get =
internal_fact ||
--- a/src/Pure/Isar/parse.ML Mon May 23 22:43:22 2016 +0200
+++ b/src/Pure/Isar/parse.ML Tue May 24 11:39:26 2016 +0200
@@ -62,8 +62,9 @@
val list: 'a parser -> 'a list parser
val list1: 'a parser -> 'a list parser
val properties: Properties.T parser
- val name: bstring parser
+ val name: string parser
val binding: binding parser
+ val embedded: string parser
val text: string parser
val path: string parser
val theory_name: string parser
@@ -257,16 +258,21 @@
val properties = $$$ "(" |-- !!! (list (string -- ($$$ "=" |-- string)) --| $$$ ")");
-(* names and text *)
+(* names and embedded content *)
val name =
- group (fn () => "name") (short_ident || long_ident || sym_ident || string || number);
+ group (fn () => "name")
+ (short_ident || long_ident || sym_ident || number || string);
val binding = position name >> Binding.make;
+val embedded =
+ group (fn () => "embedded content")
+ (short_ident || long_ident || sym_ident || number || string || cartouche);
+
val text =
group (fn () => "text")
- (short_ident || long_ident || sym_ident || string || number || verbatim || cartouche);
+ (short_ident || long_ident || sym_ident || number || string || verbatim || cartouche);
val path = group (fn () => "file name/path specification") name;
@@ -280,11 +286,11 @@
(* type classes *)
-val class = group (fn () => "type class") (inner_syntax name);
+val class = group (fn () => "type class") (inner_syntax embedded);
-val sort = group (fn () => "sort") (inner_syntax name);
+val sort = group (fn () => "sort") (inner_syntax embedded);
-val type_const = inner_syntax (group (fn () => "type constructor") name);
+val type_const = group (fn () => "type constructor") (inner_syntax embedded);
val arity = type_const -- ($$$ "::" |-- !!!
(Scan.optional ($$$ "(" |-- !!! (list1 sort --| $$$ ")")) [] -- sort)) >> Scan.triple2;
@@ -297,7 +303,8 @@
val typ_group =
group (fn () => "type")
- (short_ident || long_ident || sym_ident || type_ident || type_var || string || number);
+ (short_ident || long_ident || sym_ident || type_ident || type_var || number ||
+ string || cartouche);
val typ = inner_syntax typ_group;
@@ -386,15 +393,13 @@
(* terms *)
-val tm = short_ident || long_ident || sym_ident || term_var || number || string;
-
-val term_group = group (fn () => "term") tm;
-val prop_group = group (fn () => "proposition") tm;
+val term_group = group (fn () => "term") (term_var || embedded);
+val prop_group = group (fn () => "proposition") (term_var || embedded);
val term = inner_syntax term_group;
val prop = inner_syntax prop_group;
-val const = inner_syntax (group (fn () => "constant") name);
+val const = group (fn () => "constant") (inner_syntax embedded);
val literal_fact = inner_syntax (group (fn () => "literal fact") (alt_string || cartouche));
--- a/src/Pure/ML/ml_antiquotations.ML Mon May 23 22:43:22 2016 +0200
+++ b/src/Pure/ML/ml_antiquotations.ML Tue May 24 11:39:26 2016 +0200
@@ -17,7 +17,7 @@
(Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")") #>
ML_Antiquotation.declaration @{binding print}
- (Scan.lift (Scan.optional Args.name "Output.writeln"))
+ (Scan.lift (Scan.optional Args.embedded "Output.writeln"))
(fn src => fn output => fn ctxt =>
let
val struct_name = ML_Context.struct_name ctxt;
@@ -86,7 +86,7 @@
(* type classes *)
-fun class syn = Args.context -- Scan.lift Args.name_inner_syntax >> (fn (ctxt, s) =>
+fun class syn = Args.context -- Scan.lift Args.embedded_inner_syntax >> (fn (ctxt, s) =>
Proof_Context.read_class ctxt s
|> syn ? Lexicon.mark_class
|> ML_Syntax.print_string);
@@ -96,13 +96,13 @@
ML_Antiquotation.inline @{binding class_syntax} (class true) #>
ML_Antiquotation.inline @{binding sort}
- (Args.context -- Scan.lift Args.name_inner_syntax >> (fn (ctxt, s) =>
+ (Args.context -- Scan.lift Args.embedded_inner_syntax >> (fn (ctxt, s) =>
ML_Syntax.atomic (ML_Syntax.print_sort (Syntax.read_sort ctxt s)))));
(* type constructors *)
-fun type_name kind check = Args.context -- Scan.lift (Parse.position Args.name_inner_syntax)
+fun type_name kind check = Args.context -- Scan.lift (Parse.position Args.embedded_inner_syntax)
>> (fn (ctxt, (s, pos)) =>
let
val Type (c, _) = Proof_Context.read_type_name {proper = true, strict = false} ctxt s;
@@ -126,7 +126,7 @@
(* constants *)
-fun const_name check = Args.context -- Scan.lift (Parse.position Args.name_inner_syntax)
+fun const_name check = Args.context -- Scan.lift (Parse.position Args.embedded_inner_syntax)
>> (fn (ctxt, (s, pos)) =>
let
val Const (c, _) = Proof_Context.read_const {proper = true, strict = false} ctxt s;
@@ -143,13 +143,13 @@
(const_name (fn (_, c) => Lexicon.mark_const c)) #>
ML_Antiquotation.inline @{binding syntax_const}
- (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (c, pos)) =>
+ (Args.context -- Scan.lift (Parse.position Args.embedded) >> (fn (ctxt, (c, pos)) =>
if is_some (Syntax.lookup_const (Proof_Context.syn_of ctxt) c)
then ML_Syntax.print_string c
else error ("Unknown syntax const: " ^ quote c ^ Position.here pos))) #>
ML_Antiquotation.inline @{binding const}
- (Args.context -- Scan.lift (Parse.position Args.name_inner_syntax) -- Scan.optional
+ (Args.context -- Scan.lift (Parse.position Args.embedded_inner_syntax) -- Scan.optional
(Scan.lift (Args.$$$ "(") |-- Parse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) []
>> (fn ((ctxt, (raw_c, pos)), Ts) =>
let
--- a/src/Pure/ML/ml_thms.ML Mon May 23 22:43:22 2016 +0200
+++ b/src/Pure/ML/ml_thms.ML Tue May 24 11:39:26 2016 +0200
@@ -77,7 +77,7 @@
val and_ = Args.$$$ "and";
val by = Parse.reserved "by";
-val goal = Scan.unless (by || and_) Args.name_inner_syntax;
+val goal = Scan.unless (by || and_) Args.embedded_inner_syntax;
val _ = Theory.setup
(ML_Antiquotation.declaration @{binding lemma}
--- a/src/Pure/Thy/document_antiquotations.ML Mon May 23 22:43:22 2016 +0200
+++ b/src/Pure/Thy/document_antiquotations.ML Tue May 24 11:39:26 2016 +0200
@@ -195,7 +195,7 @@
(* URLs *)
val _ = Theory.setup
- (Thy_Output.antiquotation @{binding url} (Scan.lift (Parse.position Parse.name))
+ (Thy_Output.antiquotation @{binding url} (Scan.lift (Parse.position Parse.embedded))
(fn {context = ctxt, ...} => fn (name, pos) =>
(Context_Position.reports ctxt [(pos, Markup.language_path), (pos, Markup.url name)];
enclose "\\url{" "}" name)));
--- a/src/Pure/Thy/thy_output.ML Mon May 23 22:43:22 2016 +0200
+++ b/src/Pure/Thy/thy_output.ML Tue May 24 11:39:26 2016 +0200
@@ -645,10 +645,10 @@
basic_entity @{binding term_type} (Term_Style.parse -- Args.term) pretty_term_typ #>
basic_entity @{binding typeof} (Term_Style.parse -- Args.term) pretty_term_typeof #>
basic_entity @{binding const} (Args.const {proper = true, strict = false}) pretty_const #>
- basic_entity @{binding abbrev} (Scan.lift Args.name_inner_syntax) pretty_abbrev #>
+ basic_entity @{binding abbrev} (Scan.lift Args.embedded_inner_syntax) pretty_abbrev #>
basic_entity @{binding typ} Args.typ_abbrev Syntax.pretty_typ #>
- basic_entity @{binding class} (Scan.lift Args.name_inner_syntax) pretty_class #>
- basic_entity @{binding type} (Scan.lift Args.name) pretty_type #>
+ basic_entity @{binding class} (Scan.lift Args.embedded_inner_syntax) pretty_class #>
+ basic_entity @{binding type} (Scan.lift Args.embedded) pretty_type #>
basic_entities @{binding prf} Attrib.thms (pretty_prf false) #>
basic_entities @{binding full_prf} Attrib.thms (pretty_prf true) #>
basic_entity @{binding theory} (Scan.lift (Parse.position Args.name)) pretty_theory);
--- a/src/Pure/Tools/rule_insts.ML Mon May 23 22:43:22 2016 +0200
+++ b/src/Pure/Tools/rule_insts.ML Tue May 24 11:39:26 2016 +0200
@@ -177,7 +177,8 @@
(* where: named instantiation *)
val named_insts =
- Parse.and_list1 (Parse.position Args.var -- (Args.$$$ "=" |-- Parse.!!! Args.name_inner_syntax))
+ Parse.and_list1
+ (Parse.position Args.var -- (Args.$$$ "=" |-- Parse.!!! Args.embedded_inner_syntax))
-- Parse.for_fixes;
val _ = Theory.setup
@@ -191,7 +192,7 @@
local
-val inst = Args.maybe Args.name_inner_syntax;
+val inst = Args.maybe Args.embedded_inner_syntax;
val concl = Args.$$$ "concl" -- Args.colon;
val insts =
@@ -330,12 +331,12 @@
Method.setup @{binding cut_tac} (method cut_inst_tac (K cut_rules_tac))
"cut rule (dynamic instantiation)" #>
Method.setup @{binding subgoal_tac}
- (Args.goal_spec -- Scan.lift (Scan.repeat1 Args.name_inner_syntax -- Parse.for_fixes) >>
+ (Args.goal_spec -- Scan.lift (Scan.repeat1 Args.embedded_inner_syntax -- Parse.for_fixes) >>
(fn (quant, (props, fixes)) => fn ctxt =>
SIMPLE_METHOD'' quant (EVERY' (map (fn prop => subgoal_tac ctxt prop fixes) props))))
"insert subgoal (dynamic instantiation)" #>
Method.setup @{binding thin_tac}
- (Args.goal_spec -- Scan.lift (Args.name_inner_syntax -- Parse.for_fixes) >>
+ (Args.goal_spec -- Scan.lift (Args.embedded_inner_syntax -- Parse.for_fixes) >>
(fn (quant, (prop, fixes)) => fn ctxt => SIMPLE_METHOD'' quant (thin_tac ctxt prop fixes)))
"remove premise (dynamic instantiation)");
--- a/src/Tools/induct_tacs.ML Mon May 23 22:43:22 2016 +0200
+++ b/src/Tools/induct_tacs.ML Tue May 24 11:39:26 2016 +0200
@@ -122,14 +122,14 @@
val varss =
Parse.and_list'
- (Scan.repeat (Scan.unless rule_spec (Scan.lift (Args.maybe Args.name_inner_syntax))));
+ (Scan.repeat (Scan.unless rule_spec (Scan.lift (Args.maybe Args.embedded_inner_syntax))));
in
val _ =
Theory.setup
(Method.setup @{binding case_tac}
- (Args.goal_spec -- Scan.lift (Args.name_inner_syntax -- Parse.for_fixes) -- opt_rule >>
+ (Args.goal_spec -- Scan.lift (Args.embedded_inner_syntax -- Parse.for_fixes) -- opt_rule >>
(fn ((quant, (s, xs)), r) => fn ctxt => SIMPLE_METHOD'' quant (case_tac ctxt s xs r)))
"unstructured case analysis on types" #>
Method.setup @{binding induct_tac}
--- a/src/ZF/Tools/ind_cases.ML Mon May 23 22:43:22 2016 +0200
+++ b/src/ZF/Tools/ind_cases.ML Tue May 24 11:39:26 2016 +0200
@@ -64,7 +64,7 @@
val _ =
Theory.setup
(Method.setup @{binding "ind_cases"}
- (Scan.lift (Scan.repeat1 Args.name_inner_syntax) >>
+ (Scan.lift (Scan.repeat1 Args.embedded_inner_syntax) >>
(fn props => fn ctxt => Method.erule ctxt 0 (map (smart_cases ctxt) props)))
"dynamic case analysis on sets");
--- a/src/ZF/Tools/induct_tacs.ML Mon May 23 22:43:22 2016 +0200
+++ b/src/ZF/Tools/induct_tacs.ML Tue May 24 11:39:26 2016 +0200
@@ -179,11 +179,11 @@
val _ =
Theory.setup
(Method.setup @{binding induct_tac}
- (Args.goal_spec -- Scan.lift (Args.name -- Parse.for_fixes) >>
+ (Args.goal_spec -- Scan.lift (Args.embedded -- Parse.for_fixes) >>
(fn (quant, (s, xs)) => fn ctxt => SIMPLE_METHOD'' quant (induct_tac ctxt s xs)))
"induct_tac emulation (dynamic instantiation!)" #>
Method.setup @{binding case_tac}
- (Args.goal_spec -- Scan.lift (Args.name -- Parse.for_fixes) >>
+ (Args.goal_spec -- Scan.lift (Args.embedded -- Parse.for_fixes) >>
(fn (quant, (s, xs)) => fn ctxt => SIMPLE_METHOD'' quant (exhaust_tac ctxt s xs)))
"datatype case_tac emulation (dynamic instantiation!)");
--- a/src/ZF/UNITY/SubstAx.thy Mon May 23 22:43:22 2016 +0200
+++ b/src/ZF/UNITY/SubstAx.thy Tue May 24 11:39:26 2016 +0200
@@ -373,7 +373,7 @@
\<close>
method_setup ensures = \<open>
- Args.goal_spec -- Scan.lift Args.name_inner_syntax >>
+ Args.goal_spec -- Scan.lift Args.embedded_inner_syntax >>
(fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (ensures_tac ctxt s))
\<close> "for proving progress properties"