--- a/NEWS Wed Apr 13 14:12:51 2016 +0200
+++ b/NEWS Wed Apr 13 18:04:27 2016 +0200
@@ -16,6 +16,10 @@
INCOMPATIBILITY, need to provide explicit type constraints for Pure
types where this is really intended.
+* Simplified outer syntax: uniform category "name" includes long
+identifiers. Former "xname" / "nameref" / "name reference" has been
+discontinued.
+
* Mixfix annotations support general block properties, with syntax
"(\<open>x=a y=b z \<dots>\<close>". Notable property names are "indent", "consistent",
"unbreakable", "markup". The existing notation "(DIGITS" is equivalent
--- a/src/Doc/Datatypes/Datatypes.thy Wed Apr 13 14:12:51 2016 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy Wed Apr 13 18:04:27 2016 +0200
@@ -3020,7 +3020,7 @@
@{rail \<open>
@@{command lift_bnf} target? lb_options? \<newline>
@{syntax tyargs} name wit_terms? \<newline>
- ('via' thmref)? @{syntax map_rel}?
+ ('via' thm)? @{syntax map_rel}?
;
@{syntax_def lb_options}: '(' ((@{syntax plugins} | 'no_warn_wits') + ',') ')'
;
@@ -3055,7 +3055,7 @@
@{rail \<open>
@@{command copy_bnf} target? ('(' @{syntax plugins} ')')? \<newline>
- @{syntax tyargs} name ('via' thmref)? @{syntax map_rel}?
+ @{syntax tyargs} name ('via' thm)? @{syntax map_rel}?
\<close>}
\medskip
@@ -3203,7 +3203,7 @@
@{rail \<open>
@@{command simps_of_case} target? (name ':')? \<newline>
- (thmref + ) (@'splits' ':' (thmref + ))?
+ (thm + ) (@'splits' ':' (thm + ))?
\<close>}
\medskip
@@ -3242,7 +3242,7 @@
@{rail \<open>
@@{command case_of_simps} target? (name ':')? \<newline>
- (thmref + )
+ (thm + )
\<close>}
\medskip
--- a/src/Doc/Eisbach/Manual.thy Wed Apr 13 14:12:51 2016 +0200
+++ b/src/Doc/Eisbach/Manual.thy Wed Apr 13 18:04:27 2016 +0200
@@ -288,7 +288,7 @@
;
kind:
(@'conclusion' | @'premises' ('(' 'local' ')')? |
- '(' term ')' | @{syntax thmrefs})
+ '(' term ')' | @{syntax thms})
;
pattern: fact_name? term args? \<newline> (@'for' fixes)?
;
--- a/src/Doc/Implementation/Isar.thy Wed Apr 13 14:12:51 2016 +0200
+++ b/src/Doc/Implementation/Isar.thy Wed Apr 13 18:04:27 2016 +0200
@@ -363,7 +363,7 @@
The @{ML Attrib.thms} parser produces a list of theorems from the usual Isar
syntax involving attribute expressions etc.\ (syntax category @{syntax
- thmrefs}) @{cite "isabelle-isar-ref"}. The resulting @{ML_text thms} are
+ thms}) @{cite "isabelle-isar-ref"}. The resulting @{ML_text thms} are
added to @{ML HOL_basic_ss} which already contains the basic Simplifier
setup for HOL.
--- a/src/Doc/Implementation/Logic.thy Wed Apr 13 14:12:51 2016 +0200
+++ b/src/Doc/Implementation/Logic.thy Wed Apr 13 18:04:27 2016 +0200
@@ -171,13 +171,13 @@
\end{matharray}
@{rail \<open>
- @@{ML_antiquotation class} nameref
+ @@{ML_antiquotation class} name
;
@@{ML_antiquotation sort} sort
;
(@@{ML_antiquotation type_name} |
@@{ML_antiquotation type_abbrev} |
- @@{ML_antiquotation nonterminal}) nameref
+ @@{ML_antiquotation nonterminal}) name
;
@@{ML_antiquotation typ} type
\<close>}
@@ -392,7 +392,7 @@
@{rail \<open>
(@@{ML_antiquotation const_name} |
- @@{ML_antiquotation const_abbrev}) nameref
+ @@{ML_antiquotation const_abbrev}) name
;
@@{ML_antiquotation const} ('(' (type + ',') ')')?
;
@@ -701,9 +701,9 @@
;
@@{ML_antiquotation cprop} prop
;
- @@{ML_antiquotation thm} thmref
+ @@{ML_antiquotation thm} thm
;
- @@{ML_antiquotation thms} thmrefs
+ @@{ML_antiquotation thms} thms
;
@@{ML_antiquotation lemma} ('(' @'open' ')')? ((prop +) + @'and') \<newline>
@'by' method method?
--- a/src/Doc/Implementation/ML.thy Wed Apr 13 14:12:51 2016 +0200
+++ b/src/Doc/Implementation/ML.thy Wed Apr 13 18:04:27 2016 +0200
@@ -653,10 +653,10 @@
special syntactic entities of the following form:
@{rail \<open>
- @{syntax_def antiquote}: '@{' nameref args '}'
+ @{syntax_def antiquote}: '@{' name args '}'
\<close>}
- Here @{syntax nameref} and @{syntax args} are outer syntax categories, as
+ Here @{syntax name} and @{syntax args} are outer syntax categories, as
defined in @{cite "isabelle-isar-ref"}.
\<^medskip>
--- a/src/Doc/Implementation/Prelim.thy Wed Apr 13 14:12:51 2016 +0200
+++ b/src/Doc/Implementation/Prelim.thy Wed Apr 13 18:04:27 2016 +0200
@@ -142,9 +142,9 @@
\end{matharray}
@{rail \<open>
- @@{ML_antiquotation theory} nameref?
+ @@{ML_antiquotation theory} name?
;
- @@{ML_antiquotation theory_context} nameref
+ @@{ML_antiquotation theory_context} name
\<close>}
\<^descr> \<open>@{theory}\<close> refers to the background theory of the current context --- as
--- a/src/Doc/Isar_Ref/Document_Preparation.thy Wed Apr 13 14:12:51 2016 +0200
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy Wed Apr 13 18:04:27 2016 +0200
@@ -167,7 +167,7 @@
(@@{antiquotation text} | @@{antiquotation cartouche} | @@{antiquotation theory_text})
options @{syntax text} |
@@{antiquotation theory} options @{syntax name} |
- @@{antiquotation thm} options styles @{syntax thmrefs} |
+ @@{antiquotation thm} options styles @{syntax thms} |
@@{antiquotation lemma} options @{syntax prop} @'by' @{syntax method} @{syntax method}? |
@@{antiquotation prop} options styles @{syntax prop} |
@@{antiquotation term} options styles @{syntax term} |
@@ -185,8 +185,8 @@
@{syntax antiquotation}:
@@{antiquotation goals} options |
@@{antiquotation subgoals} options |
- @@{antiquotation prf} options @{syntax thmrefs} |
- @@{antiquotation full_prf} options @{syntax thmrefs} |
+ @@{antiquotation prf} options @{syntax thms} |
+ @@{antiquotation full_prf} options @{syntax thms} |
@@{antiquotation ML} options @{syntax text} |
@@{antiquotation ML_op} options @{syntax text} |
@@{antiquotation ML_type} options @{syntax text} |
--- a/src/Doc/Isar_Ref/Generic.thy Wed Apr 13 14:12:51 2016 +0200
+++ b/src/Doc/Isar_Ref/Generic.thy Wed Apr 13 18:04:27 2016 +0200
@@ -71,12 +71,12 @@
\end{matharray}
@{rail \<open>
- (@@{method fold} | @@{method unfold} | @@{method insert}) @{syntax thmrefs}
+ (@@{method fold} | @@{method unfold} | @@{method insert}) @{syntax thms}
;
(@@{method erule} | @@{method drule} | @@{method frule})
- ('(' @{syntax nat} ')')? @{syntax thmrefs}
+ ('(' @{syntax nat} ')')? @{syntax thms}
;
- (@@{method intro} | @@{method elim}) @{syntax thmrefs}?
+ (@@{method intro} | @@{method elim}) @{syntax thms}?
;
@@{method sleep} @{syntax real}
\<close>}
@@ -140,9 +140,9 @@
;
@@{attribute untagged} @{syntax name}
;
- @@{attribute THEN} ('[' @{syntax nat} ']')? @{syntax thmref}
+ @@{attribute THEN} ('[' @{syntax nat} ']')? @{syntax thm}
;
- (@@{attribute unfolded} | @@{attribute folded}) @{syntax thmrefs}
+ (@@{attribute unfolded} | @@{attribute folded}) @{syntax thms}
;
@@{attribute rotated} @{syntax int}?
\<close>}
@@ -192,9 +192,9 @@
\end{matharray}
@{rail \<open>
- @@{method subst} ('(' 'asm' ')')? \<newline> ('(' (@{syntax nat}+) ')')? @{syntax thmref}
+ @@{method subst} ('(' 'asm' ')')? \<newline> ('(' (@{syntax nat}+) ')')? @{syntax thm}
;
- @@{method split} @{syntax thmrefs}
+ @@{method split} @{syntax thms}
\<close>}
These methods provide low-level facilities for equational reasoning
@@ -284,7 +284,7 @@
opt: '(' ('no_asm' | 'no_asm_simp' | 'no_asm_use' | 'asm_lr' ) ')'
;
@{syntax_def simpmod}: ('add' | 'del' | 'only' | 'split' (() | 'add' | 'del') |
- 'cong' (() | 'add' | 'del')) ':' @{syntax thmrefs}
+ 'cong' (() | 'add' | 'del')) ':' @{syntax thms}
\<close>}
\<^descr> @{method simp} invokes the Simplifier on the first subgoal, after
@@ -1063,7 +1063,7 @@
\end{matharray}
@{rail \<open>
- @@{attribute simplified} opt? @{syntax thmrefs}?
+ @@{attribute simplified} opt? @{syntax thms}?
;
opt: '(' ('no_asm' | 'no_asm_simp' | 'no_asm_use') ')'
@@ -1383,7 +1383,7 @@
\end{matharray}
@{rail \<open>
- @@{method rule} @{syntax thmrefs}?
+ @@{method rule} @{syntax thms}?
\<close>}
\<^descr> @{method rule} as offered by the Classical Reasoner is a
@@ -1434,12 +1434,12 @@
@@{method deepen} (@{syntax nat} ?) (@{syntax clamod} * )
;
@{syntax_def clamod}:
- (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del') ':' @{syntax thmrefs}
+ (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del') ':' @{syntax thms}
;
@{syntax_def clasimpmod}: ('simp' (() | 'add' | 'del' | 'only') |
('cong' | 'split') (() | 'add' | 'del') |
'iff' (((() | 'add') '?'?) | 'del') |
- (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del')) ':' @{syntax thmrefs}
+ (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del')) ':' @{syntax thms}
\<close>}
\<^descr> @{method blast} is a separate classical tableau prover that
--- a/src/Doc/Isar_Ref/HOL_Specific.thy Wed Apr 13 14:12:51 2016 +0200
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy Wed Apr 13 18:04:27 2016 +0200
@@ -109,7 +109,7 @@
(@@{command (HOL) inductive} | @@{command (HOL) inductive_set} |
@@{command (HOL) coinductive} | @@{command (HOL) coinductive_set})
@{syntax "fixes"} @{syntax "for_fixes"} \<newline>
- (@'where' clauses)? (@'monos' @{syntax thmrefs})?
+ (@'where' clauses)? (@'monos' @{syntax thms})?
;
clauses: (@{syntax thmdecl}? @{syntax prop} + '|')
;
@@ -568,7 +568,7 @@
\end{matharray}
@{rail \<open>
- @@{command (HOL) partial_function} '(' @{syntax nameref} ')' @{syntax "fixes"} \<newline>
+ @@{command (HOL) partial_function} '(' @{syntax name} ')' @{syntax "fixes"} \<newline>
@'where' @{syntax thmdecl}? @{syntax prop}
\<close>}
@@ -638,7 +638,7 @@
hints: '(' @'hints' ( recdefmod * ) ')'
;
recdefmod: (('recdef_simp' | 'recdef_cong' | 'recdef_wf')
- (() | 'add' | 'del') ':' @{syntax thmrefs}) | @{syntax clasimpmod}
+ (() | 'add' | 'del') ':' @{syntax thms}) | @{syntax clasimpmod}
\<close>}
\<^descr> @{command (HOL) "recdef"} defines general well-founded
@@ -689,7 +689,7 @@
@{rail \<open>
(@@{command adhoc_overloading} | @@{command no_adhoc_overloading})
- (@{syntax nameref} (@{syntax term} + ) + @'and')
+ (@{syntax name} (@{syntax term} + ) + @'and')
\<close>}
\<^descr> @{command "adhoc_overloading"}~\<open>c v\<^sub>1 ... v\<^sub>n\<close>
@@ -1265,7 +1265,7 @@
;
quot_morphisms: @'morphisms' @{syntax name} @{syntax name}
;
- quot_parametric: @'parametric' @{syntax thmref}
+ quot_parametric: @'parametric' @{syntax thm}
\<close>}
\<^descr> @{command (HOL) "quotient_type"} defines a new quotient type \<open>\<tau>\<close>. The injection from a quotient type to a raw type is called \<open>rep_\<tau>\<close>, its inverse \<open>abs_\<tau>\<close> unless explicit @{keyword (HOL)
@@ -1321,19 +1321,19 @@
\end{matharray}
@{rail \<open>
- @@{command (HOL) setup_lifting} @{syntax thmref} @{syntax thmref}? \<newline>
- (@'parametric' @{syntax thmref})?
+ @@{command (HOL) setup_lifting} @{syntax thm} @{syntax thm}? \<newline>
+ (@'parametric' @{syntax thm})?
;
@@{command (HOL) lift_definition} ('(' 'code_dt' ')')? \<newline>
@{syntax name} '::' @{syntax type} @{syntax mixfix}? 'is' @{syntax term} \<newline>
- (@'parametric' (@{syntax thmref}+))?
+ (@'parametric' (@{syntax thm}+))?
;
- @@{command (HOL) lifting_forget} @{syntax nameref}
+ @@{command (HOL) lifting_forget} @{syntax name}
;
- @@{command (HOL) lifting_update} @{syntax nameref}
+ @@{command (HOL) lifting_update} @{syntax name}
;
@@{attribute (HOL) lifting_restore}
- @{syntax thmref} (@{syntax thmref} @{syntax thmref})?
+ @{syntax thm} (@{syntax thm} @{syntax thm})?
\<close>}
\<^descr> @{command (HOL) "setup_lifting"} Sets up the Lifting package to work
@@ -1661,9 +1661,9 @@
;
constdecl: @{syntax name} ('::' @{syntax type})? @{syntax mixfix}?
;
- @@{method (HOL) lifting} @{syntax thmrefs}?
+ @@{method (HOL) lifting} @{syntax thms}?
;
- @@{method (HOL) lifting_setup} @{syntax thmrefs}?
+ @@{method (HOL) lifting_setup} @{syntax thms}?
\<close>}
\<^descr> @{command (HOL) "quotient_definition"} defines a constant on the
@@ -1750,7 +1750,7 @@
@@{command (HOL) try}
;
- @@{command (HOL) try0} ( ( ( 'simp' | 'intro' | 'elim' | 'dest' ) ':' @{syntax thmrefs} ) + ) ?
+ @@{command (HOL) try0} ( ( ( 'simp' | 'intro' | 'elim' | 'dest' ) ':' @{syntax thms} ) + ) ?
@{syntax nat}?
;
@@ -1761,7 +1761,7 @@
;
args: ( @{syntax name} '=' value + ',' )
;
- facts: '(' ( ( ( ( 'add' | 'del' ) ':' ) ? @{syntax thmrefs} ) + ) ? ')'
+ facts: '(' ( ( ( ( 'add' | 'del' ) ':' ) ? @{syntax thms} ) + ) ? ')'
\<close>} % FIXME check args "value"
\<^descr> @{command (HOL) "solve_direct"} checks whether the current
@@ -1822,7 +1822,7 @@
@@{command (HOL) nitpick_params}) ( '[' args ']' )?
;
- @@{command (HOL) quickcheck_generator} @{syntax nameref} \<newline>
+ @@{command (HOL) quickcheck_generator} @{syntax name} \<newline>
'operations:' ( @{syntax term} +)
;
@@ -2140,11 +2140,11 @@
\end{matharray}
@{rail \<open>
- @@{method (HOL) meson} @{syntax thmrefs}?
+ @@{method (HOL) meson} @{syntax thms}?
;
@@{method (HOL) metis}
('(' ('partial_types' | 'full_types' | 'no_types' | @{syntax name}) ')')?
- @{syntax thmrefs}?
+ @{syntax thms}?
\<close>}
\<^descr> @{method (HOL) meson} implements Loveland's model elimination
@@ -2170,8 +2170,8 @@
@{rail \<open>
@@{method (HOL) algebra}
- ('add' ':' @{syntax thmrefs})?
- ('del' ':' @{syntax thmrefs})?
+ ('add' ':' @{syntax thms})?
+ ('del' ':' @{syntax thms})?
;
@@{attribute (HOL) algebra} (() | 'add' | 'del')
\<close>}
@@ -2246,7 +2246,7 @@
\end{matharray}
@{rail \<open>
- @@{method (HOL) coherent} @{syntax thmrefs}?
+ @@{method (HOL) coherent} @{syntax thms}?
\<close>}
\<^descr> @{method (HOL) coherent} solves problems of \<^emph>\<open>Coherent
@@ -2279,7 +2279,7 @@
;
@@{command (HOL) inductive_cases} (@{syntax thmdecl}? (@{syntax prop}+) + @'and')
;
- rule: 'rule' ':' @{syntax thmref}
+ rule: 'rule' ':' @{syntax thm}
\<close>}
\<^descr> @{method (HOL) case_tac} and @{method (HOL) induct_tac} admit
@@ -2379,9 +2379,9 @@
;
constexpr: ( const | 'name._' | '_' )
;
- typeconstructor: @{syntax nameref}
+ typeconstructor: @{syntax name}
;
- class: @{syntax nameref}
+ class: @{syntax name}
;
target: 'SML' | 'OCaml' | 'Haskell' | 'Scala' | 'Eval'
;
--- a/src/Doc/Isar_Ref/Inner_Syntax.thy Wed Apr 13 14:12:51 2016 +0200
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy Wed Apr 13 18:04:27 2016 +0200
@@ -53,9 +53,9 @@
;
@@{command prop} @{syntax modes}? @{syntax prop}
;
- @@{command thm} @{syntax modes}? @{syntax thmrefs}
+ @@{command thm} @{syntax modes}? @{syntax thms}
;
- ( @@{command prf} | @@{command full_prf} ) @{syntax modes}? @{syntax thmrefs}?
+ ( @@{command prf} | @@{command full_prf} ) @{syntax modes}? @{syntax thms}?
;
@@{command print_state} @{syntax modes}?
;
@@ -504,12 +504,12 @@
@{rail \<open>
(@@{command type_notation} | @@{command no_type_notation}) @{syntax mode}? \<newline>
- (@{syntax nameref} @{syntax mixfix} + @'and')
+ (@{syntax name} @{syntax mixfix} + @'and')
;
(@@{command notation} | @@{command no_notation}) @{syntax mode}? \<newline>
- (@{syntax nameref} @{syntax mixfix} + @'and')
+ (@{syntax name} @{syntax mixfix} + @'and')
;
- @@{command write} @{syntax mode}? (@{syntax nameref} @{syntax mixfix} + @'and')
+ @@{command write} @{syntax mode}? (@{syntax name} @{syntax mixfix} + @'and')
\<close>}
\<^descr> @{command "type_notation"}~\<open>c (mx)\<close> associates mixfix syntax with an
@@ -1103,7 +1103,7 @@
;
mode: ('(' ( @{syntax name} | @'output' | @{syntax name} @'output' ) ')')
;
- transpat: ('(' @{syntax nameref} ')')? @{syntax string}
+ transpat: ('(' @{syntax name} ')')? @{syntax string}
\<close>}
\<^descr> @{command "nonterminal"}~\<open>c\<close> declares a type constructor \<open>c\<close> (without
--- a/src/Doc/Isar_Ref/Outer_Syntax.thy Wed Apr 13 14:12:51 2016 +0200
+++ b/src/Doc/Isar_Ref/Outer_Syntax.thy Wed Apr 13 18:04:27 2016 +0200
@@ -179,19 +179,14 @@
text \<open>
Entity @{syntax name} usually refers to any name of types, constants,
- theorems etc.\ that are to be \<^emph>\<open>declared\<close> or \<^emph>\<open>defined\<close> (so qualified
- identifiers are excluded here). Quoted strings provide an escape for
- non-identifier names or those ruled out by outer syntax keywords (e.g.\
- quoted \<^verbatim>\<open>"let"\<close>). Already existing objects are usually referenced by
- @{syntax nameref}.
+ theorems etc.\ Quoted strings provide an escape for non-identifier names or
+ those ruled out by outer syntax keywords (e.g.\ quoted \<^verbatim>\<open>"let"\<close>).
@{rail \<open>
- @{syntax_def name}: @{syntax ident} | @{syntax symident} |
- @{syntax string} | @{syntax nat}
+ @{syntax_def name}: @{syntax ident} | @{syntax longident} |
+ @{syntax symident} | @{syntax string} | @{syntax nat}
;
@{syntax_def par_name}: '(' @{syntax name} ')'
- ;
- @{syntax_def nameref}: @{syntax name} | @{syntax longident}
\<close>}
\<close>
@@ -219,13 +214,13 @@
text \<open>
Large chunks of plain @{syntax text} are usually given @{syntax verbatim},
i.e.\ enclosed in \<^verbatim>\<open>{*\<close>~\<open>\<dots>\<close>~\<^verbatim>\<open>*}\<close>, or as @{syntax cartouche} \<open>\<open>\<dots>\<close>\<close>. For
- convenience, any of the smaller text units conforming to @{syntax nameref}
- are admitted as well. A marginal @{syntax comment} is of the form
- \<^verbatim>\<open>--\<close>~@{syntax text} or \<^verbatim>\<open>\<comment>\<close>~@{syntax text}. Any number of these may occur
- within Isabelle/Isar commands.
+ convenience, any of the smaller text units conforming to @{syntax name} are
+ admitted as well. A marginal @{syntax comment} is of the form \<^verbatim>\<open>--\<close>~@{syntax
+ text} or \<^verbatim>\<open>\<comment>\<close>~@{syntax text}. Any number of these may occur within
+ Isabelle/Isar commands.
@{rail \<open>
- @{syntax_def text}: @{syntax verbatim} | @{syntax cartouche} | @{syntax nameref}
+ @{syntax_def text}: @{syntax verbatim} | @{syntax cartouche} | @{syntax name}
;
@{syntax_def comment}: ('--' | @'\<comment>') @{syntax text}
\<close>}
@@ -241,9 +236,9 @@
directly at the outer level.
@{rail \<open>
- @{syntax_def classdecl}: @{syntax name} (('<' | '\<subseteq>') (@{syntax nameref} + ','))?
+ @{syntax_def classdecl}: @{syntax name} (('<' | '\<subseteq>') (@{syntax name} + ','))?
;
- @{syntax_def sort}: @{syntax nameref}
+ @{syntax_def sort}: @{syntax name}
;
@{syntax_def arity}: ('(' (@{syntax sort} + ',') ')')? @{syntax sort}
\<close>}
@@ -265,10 +260,10 @@
as \<^verbatim>\<open>=\<close> or \<^verbatim>\<open>+\<close>).
@{rail \<open>
- @{syntax_def type}: @{syntax nameref} | @{syntax typefree} |
+ @{syntax_def type}: @{syntax name} | @{syntax typefree} |
@{syntax typevar}
;
- @{syntax_def term}: @{syntax nameref} | @{syntax var}
+ @{syntax_def term}: @{syntax name} | @{syntax var}
;
@{syntax_def prop}: @{syntax term}
\<close>}
@@ -377,7 +372,7 @@
conforming to @{syntax symident}.
@{rail \<open>
- @{syntax_def atom}: @{syntax nameref} | @{syntax typefree} |
+ @{syntax_def atom}: @{syntax name} | @{syntax typefree} |
@{syntax typevar} | @{syntax var} | @{syntax nat} | @{syntax float} |
@{syntax keyword} | @{syntax cartouche}
;
@@ -385,13 +380,13 @@
;
@{syntax_def args}: arg *
;
- @{syntax_def attributes}: '[' (@{syntax nameref} @{syntax args} * ',') ']'
+ @{syntax_def attributes}: '[' (@{syntax name} @{syntax args} * ',') ']'
\<close>}
Theorem specifications come in several flavors: @{syntax axmdecl} and
@{syntax thmdecl} usually refer to axioms, assumptions or results of goal
statements, while @{syntax thmdef} collects lists of existing theorems.
- Existing theorems are given by @{syntax thmref} and @{syntax thmrefs}, the
+ Existing theorems are given by @{syntax thm} and @{syntax thms}, the
former requires an actual singleton result.
There are three forms of theorem references:
@@ -426,12 +421,12 @@
;
@{syntax_def thmdef}: thmbind '='
;
- @{syntax_def thmref}:
- (@{syntax nameref} selection? | @{syntax altstring} | @{syntax cartouche})
+ @{syntax_def thm}:
+ (@{syntax name} selection? | @{syntax altstring} | @{syntax cartouche})
@{syntax attributes}? |
'[' @{syntax attributes} ']'
;
- @{syntax_def thmrefs}: @{syntax thmref} +
+ @{syntax_def thms}: @{syntax thm} +
;
selection: '(' ((@{syntax nat} | @{syntax nat} '-' @{syntax nat}?) + ',') ')'
\<close>}
@@ -465,13 +460,13 @@
;
@@{command find_theorems} ('(' @{syntax nat}? 'with_dups'? ')')? \<newline> (thm_criterion*)
;
- thm_criterion: ('-'?) ('name' ':' @{syntax nameref} | 'intro' | 'elim' | 'dest' |
+ thm_criterion: ('-'?) ('name' ':' @{syntax name} | 'intro' | 'elim' | 'dest' |
'solves' | 'simp' ':' @{syntax term} | @{syntax term})
;
@@{command find_consts} (const_criterion*)
;
const_criterion: ('-'?)
- ('name' ':' @{syntax nameref} | 'strict' ':' @{syntax type} | @{syntax type})
+ ('name' ':' @{syntax name} | 'strict' ':' @{syntax type} | @{syntax type})
;
@@{command thm_deps} @{syntax thmrefs}
;
--- a/src/Doc/Isar_Ref/Proof.thy Wed Apr 13 14:12:51 2016 +0200
+++ b/src/Doc/Isar_Ref/Proof.thy Wed Apr 13 18:04:27 2016 +0200
@@ -283,10 +283,10 @@
claim.
@{rail \<open>
- @@{command note} (@{syntax thmdef}? @{syntax thmrefs} + @'and')
+ @@{command note} (@{syntax thmdef}? @{syntax thms} + @'and')
;
(@@{command from} | @@{command with} | @@{command using} | @@{command unfolding})
- (@{syntax thmrefs} + @'and')
+ (@{syntax thms} + @'and')
\<close>}
\<^descr> @{command "note"}~\<open>a = b\<^sub>1 \<dots> b\<^sub>n\<close> recalls existing facts \<open>b\<^sub>1, \<dots>, b\<^sub>n\<close>,
@@ -386,7 +386,7 @@
(@@{command have} | @@{command show} | @@{command hence} | @@{command thus})
stmt cond_stmt @{syntax for_fixes}
;
- @@{command print_statement} @{syntax modes}? @{syntax thmrefs}
+ @@{command print_statement} @{syntax modes}? @{syntax thms}
;
stmt: (@{syntax props} + @'and')
@@ -513,7 +513,7 @@
\end{matharray}
@{rail \<open>
- (@@{command also} | @@{command finally}) ('(' @{syntax thmrefs} ')')?
+ (@@{command also} | @@{command finally}) ('(' @{syntax thms} ')')?
;
@@{attribute trans} (() | 'add' | 'del')
\<close>}
@@ -571,16 +571,16 @@
``\<^verbatim>\<open>|\<close>'' (alternative choices), ``\<^verbatim>\<open>?\<close>'' (try), ``\<^verbatim>\<open>+\<close>'' (repeat at least
once), ``\<^verbatim>\<open>[\<close>\<open>n\<close>\<^verbatim>\<open>]\<close>'' (restriction to first \<open>n\<close> subgoals). In practice,
proof methods are usually just a comma separated list of @{syntax
- nameref}~@{syntax args} specifications. Note that parentheses may be dropped
+ name}~@{syntax args} specifications. Note that parentheses may be dropped
for single method specifications (with no arguments). The syntactic
precedence of method combinators is \<^verbatim>\<open>|\<close> \<^verbatim>\<open>;\<close> \<^verbatim>\<open>,\<close> \<^verbatim>\<open>[]\<close> \<^verbatim>\<open>+\<close> \<^verbatim>\<open>?\<close> (from low
to high).
@{rail \<open>
@{syntax_def method}:
- (@{syntax nameref} | '(' methods ')') (() | '?' | '+' | '[' @{syntax nat}? ']')
+ (@{syntax name} | '(' methods ')') (() | '?' | '+' | '[' @{syntax nat}? ']')
;
- methods: (@{syntax nameref} @{syntax args} | @{syntax method}) + (',' | ';' | '|')
+ methods: (@{syntax name} @{syntax args} | @{syntax method}) + (',' | ';' | '|')
\<close>}
Regular Isar proof methods do \<^emph>\<open>not\<close> admit direct goal addressing, but refer
@@ -753,19 +753,19 @@
@{rail \<open>
@@{method goal_cases} (@{syntax name}*)
;
- @@{method fact} @{syntax thmrefs}?
+ @@{method fact} @{syntax thms}?
;
- @@{method (Pure) rule} @{syntax thmrefs}?
+ @@{method (Pure) rule} @{syntax thms}?
;
rulemod: ('intro' | 'elim' | 'dest')
- ((('!' | () | '?') @{syntax nat}?) | 'del') ':' @{syntax thmrefs}
+ ((('!' | () | '?') @{syntax nat}?) | 'del') ':' @{syntax thms}
;
(@@{attribute intro} | @@{attribute elim} | @@{attribute dest})
('!' | () | '?') @{syntax nat}?
;
@@{attribute (Pure) rule} 'del'
;
- @@{attribute OF} @{syntax thmrefs}
+ @@{attribute OF} @{syntax thms}
;
@@{attribute of} @{syntax insts} ('concl' ':' @{syntax insts})? @{syntax for_fixes}
;
@@ -968,7 +968,7 @@
advanced case analysis later.
@{rail \<open>
- @@{command case} @{syntax thmdecl}? (nameref | '(' nameref (('_' | @{syntax name}) *) ')')
+ @@{command case} @{syntax thmdecl}? (name | '(' name (('_' | @{syntax name}) *) ')')
;
@@{attribute case_names} ((@{syntax name} ( '[' (('_' | @{syntax name}) +) ']' ) ? ) +)
;
@@ -1076,7 +1076,7 @@
@@{method coinduct} @{syntax insts} taking rule?
;
- rule: ('type' | 'pred' | 'set') ':' (@{syntax nameref} +) | 'rule' ':' (@{syntax thmref} +)
+ rule: ('type' | 'pred' | 'set') ':' (@{syntax name} +) | 'rule' ':' (@{syntax thm} +)
;
definst: @{syntax name} ('==' | '\<equiv>') @{syntax term} | '(' @{syntax term} ')' | @{syntax inst}
;
@@ -1253,7 +1253,7 @@
@@{attribute coinduct} spec
;
- spec: (('type' | 'pred' | 'set') ':' @{syntax nameref}) | 'del'
+ spec: (('type' | 'pred' | 'set') ':' @{syntax name}) | 'del'
\<close>}
\<^descr> @{command "print_induct_rules"} prints cases and induct rules for
--- a/src/Doc/Isar_Ref/Proof_Script.thy Wed Apr 13 14:12:51 2016 +0200
+++ b/src/Doc/Isar_Ref/Proof_Script.thy Wed Apr 13 18:04:27 2016 +0200
@@ -37,7 +37,7 @@
\end{matharray}
@{rail \<open>
- @@{command supply} (@{syntax thmdef}? @{syntax thmrefs} + @'and')
+ @@{command supply} (@{syntax thmdef}? @{syntax thms} + @'and')
;
( @@{command apply} | @@{command apply_end} ) @{syntax method}
;
@@ -222,7 +222,7 @@
@{rail \<open>
(@@{method rule_tac} | @@{method erule_tac} | @@{method drule_tac} |
@@{method frule_tac} | @@{method cut_tac}) @{syntax goal_spec}? \<newline>
- (@{syntax named_insts} @{syntax for_fixes} @'in' @{syntax thmref} | @{syntax thmrefs} )
+ (@{syntax named_insts} @{syntax for_fixes} @'in' @{syntax thm} | @{syntax thms} )
;
@@{method thin_tac} @{syntax goal_spec}? @{syntax prop} @{syntax for_fixes}
;
--- a/src/Doc/Isar_Ref/Spec.thy Wed Apr 13 14:12:51 2016 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy Wed Apr 13 18:04:27 2016 +0200
@@ -137,11 +137,11 @@
\<^theory_text>\<open>instantiation\<close>, \<^theory_text>\<open>overloading\<close>.
@{rail \<open>
- @@{command context} @{syntax nameref} @'begin'
+ @@{command context} @{syntax name} @'begin'
;
@@{command context} @{syntax_ref "includes"}? (@{syntax context_elem} * ) @'begin'
;
- @{syntax_def target}: '(' @'in' @{syntax nameref} ')'
+ @{syntax_def target}: '(' @'in' @{syntax name} ')'
\<close>}
\<^descr> \<^theory_text>\<open>context c begin\<close> opens a named context, by recommencing an existing
@@ -226,13 +226,13 @@
(\secref{sec:locale}).
@{rail \<open>
- @@{command bundle} @{syntax name} '=' @{syntax thmrefs} @{syntax for_fixes}
+ @@{command bundle} @{syntax name} '=' @{syntax thms} @{syntax for_fixes}
;
@@{command print_bundles} ('!'?)
;
- (@@{command include} | @@{command including}) (@{syntax nameref}+)
+ (@@{command include} | @@{command including}) (@{syntax name}+)
;
- @{syntax_def "includes"}: @'includes' (@{syntax nameref}+)
+ @{syntax_def "includes"}: @'includes' (@{syntax name}+)
\<close>}
\<^descr> \<^theory_text>\<open>bundle b = decls\<close> defines a bundle of declarations in the current
@@ -383,7 +383,7 @@
(@@{command declaration} | @@{command syntax_declaration})
('(' @'pervasive' ')')? \<newline> @{syntax text}
;
- @@{command declare} (@{syntax thmrefs} + @'and')
+ @@{command declare} (@{syntax thms} + @'and')
\<close>}
\<^descr> \<^theory_text>\<open>declaration d\<close> adds the declaration function \<open>d\<close> of ML type @{ML_type
@@ -440,7 +440,7 @@
@{rail \<open>
@{syntax_def locale_expr}: (instance + '+') @{syntax for_fixes}
;
- instance: (qualifier ':')? @{syntax nameref} (pos_insts | named_insts)
+ instance: (qualifier ':')? @{syntax name} (pos_insts | named_insts)
;
qualifier: @{syntax name} ('?')?
;
@@ -490,7 +490,7 @@
;
@@{command experiment} (@{syntax context_elem}*) @'begin'
;
- @@{command print_locale} '!'? @{syntax nameref}
+ @@{command print_locale} '!'? @{syntax name}
;
@@{command print_locales} ('!'?)
;
@@ -502,7 +502,7 @@
@'constrains' (@{syntax name} '::' @{syntax type} + @'and') |
@'assumes' (@{syntax props} + @'and') |
@'defines' (@{syntax thmdecl}? @{syntax prop} @{syntax prop_pat}? + @'and') |
- @'notes' (@{syntax thmdef}? @{syntax thmrefs} + @'and')
+ @'notes' (@{syntax thmdef}? @{syntax thms} + @'and')
\<close>}
\<^descr> \<^theory_text>\<open>locale loc = import + body\<close> defines a new locale \<open>loc\<close> as a context
@@ -628,12 +628,12 @@
@@{command global_interpretation} @{syntax locale_expr} \<newline>
definitions? equations?
;
- @@{command sublocale} (@{syntax nameref} ('<' | '\<subseteq>'))? @{syntax locale_expr} \<newline>
+ @@{command sublocale} (@{syntax name} ('<' | '\<subseteq>'))? @{syntax locale_expr} \<newline>
definitions? equations?
;
@@{command print_dependencies} '!'? @{syntax locale_expr}
;
- @@{command print_interps} @{syntax nameref}
+ @@{command print_interps} @{syntax name}
;
definitions: @'defines' (@{syntax thmdecl}? @{syntax name} \<newline>
@@ -798,15 +798,15 @@
@@{command class} class_spec @'begin'?
;
class_spec: @{syntax name} '='
- ((@{syntax nameref} '+' (@{syntax context_elem}+)) |
- @{syntax nameref} | (@{syntax context_elem}+))
+ ((@{syntax name} '+' (@{syntax context_elem}+)) |
+ @{syntax name} | (@{syntax context_elem}+))
;
- @@{command instantiation} (@{syntax nameref} + @'and') '::' @{syntax arity} @'begin'
+ @@{command instantiation} (@{syntax name} + @'and') '::' @{syntax arity} @'begin'
;
- @@{command instance} (() | (@{syntax nameref} + @'and') '::' @{syntax arity} |
- @{syntax nameref} ('<' | '\<subseteq>') @{syntax nameref} )
+ @@{command instance} (() | (@{syntax name} + @'and') '::' @{syntax arity} |
+ @{syntax name} ('<' | '\<subseteq>') @{syntax name} )
;
- @@{command subclass} @{syntax nameref}
+ @@{command subclass} @{syntax name}
;
@@{command class_deps} (class_bounds class_bounds?)?
;
@@ -1231,7 +1231,7 @@
\end{matharray}
@{rail \<open>
- @@{command lemmas} (@{syntax thmdef}? @{syntax thmrefs} + @'and')
+ @@{command lemmas} (@{syntax thmdef}? @{syntax thms} + @'and')
@{syntax for_fixes}
;
@@{command named_theorems} (@{syntax name} @{syntax text}? + @'and')
@@ -1299,7 +1299,7 @@
@{rail \<open>
( @{command hide_class} | @{command hide_type} |
- @{command hide_const} | @{command hide_fact} ) ('(' @'open' ')')? (@{syntax nameref} + )
+ @{command hide_const} | @{command hide_fact} ) ('(' @'open' ')')? (@{syntax name} + )
\<close>}
Isabelle organizes any kind of name declarations (of types, constants,
--- a/src/Doc/JEdit/JEdit.thy Wed Apr 13 14:12:51 2016 +0200
+++ b/src/Doc/JEdit/JEdit.thy Wed Apr 13 18:04:27 2016 +0200
@@ -1068,7 +1068,7 @@
single criterium has the following syntax:
@{rail \<open>
- ('-'?) ('name' ':' @{syntax nameref} | 'intro' | 'elim' | 'dest' |
+ ('-'?) ('name' ':' @{syntax name} | 'intro' | 'elim' | 'dest' |
'solves' | 'simp' ':' @{syntax term} | @{syntax term})
\<close>}
@@ -1086,7 +1086,7 @@
@{rail \<open>
('-'?)
- ('name' ':' @{syntax nameref} | 'strict' ':' @{syntax type} | @{syntax type})
+ ('name' ':' @{syntax name} | 'strict' ':' @{syntax type} | @{syntax type})
\<close>}
See also the Isar command @{command_ref find_consts} in @{cite
--- a/src/Doc/Logics_ZF/ZF_Isar.thy Wed Apr 13 14:12:51 2016 +0200
+++ b/src/Doc/Logics_ZF/ZF_Isar.thy Wed Apr 13 18:04:27 2016 +0200
@@ -69,13 +69,13 @@
hints: @{syntax (ZF) "monos"}? condefs? \<newline>
@{syntax (ZF) typeintros}? @{syntax (ZF) typeelims}?
;
- @{syntax_def (ZF) "monos"}: @'monos' @{syntax thmrefs}
+ @{syntax_def (ZF) "monos"}: @'monos' @{syntax thms}
;
- condefs: @'con_defs' @{syntax thmrefs}
+ condefs: @'con_defs' @{syntax thms}
;
- @{syntax_def (ZF) typeintros}: @'type_intros' @{syntax thmrefs}
+ @{syntax_def (ZF) typeintros}: @'type_intros' @{syntax thms}
;
- @{syntax_def (ZF) typeelims}: @'type_elims' @{syntax thmrefs}
+ @{syntax_def (ZF) typeelims}: @'type_elims' @{syntax thms}
\<close>}
In the following syntax specification @{text "monos"}, @{text
--- a/src/HOL/Decision_Procs/approximation.ML Wed Apr 13 14:12:51 2016 +0200
+++ b/src/HOL/Decision_Procs/approximation.ML Wed Apr 13 18:04:27 2016 +0200
@@ -244,7 +244,7 @@
end |> Pretty.writeln;
val opt_modes =
- Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) [];
+ Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.name --| @{keyword ")"})) [];
val _ =
Outer_Syntax.command @{command_keyword approximate} "print approximation of term"
--- a/src/HOL/Library/rewrite.ML Wed Apr 13 14:12:51 2016 +0200
+++ b/src/HOL/Library/rewrite.ML Wed Apr 13 18:04:27 2016 +0200
@@ -442,7 +442,7 @@
val to_parser = Scan.option ((Args.$$$ "to") |-- Parse.term)
val subst_parser =
- let val scan = raw_pattern -- to_parser -- Parse.xthms1
+ let val scan = raw_pattern -- to_parser -- Parse.thms1
in context_lift scan prep_args end
in
Method.setup @{binding rewrite} (subst_parser >>
--- a/src/HOL/Library/simps_case_conv.ML Wed Apr 13 14:12:51 2016 +0200
+++ b/src/HOL/Library/simps_case_conv.ML Wed Apr 13 18:04:27 2016 +0200
@@ -231,15 +231,15 @@
val _ =
Outer_Syntax.local_theory @{command_keyword case_of_simps}
"turn a list of equations into a case expression"
- (Parse_Spec.opt_thm_name ":" -- Parse.xthms1 >> case_of_simps_cmd)
+ (Parse_Spec.opt_thm_name ":" -- Parse.thms1 >> case_of_simps_cmd)
val parse_splits = @{keyword "("} |-- Parse.reserved "splits" |-- @{keyword ":"} |--
- Parse.xthms1 --| @{keyword ")"}
+ Parse.thms1 --| @{keyword ")"}
val _ =
Outer_Syntax.local_theory @{command_keyword simps_of_case}
"perform case split on rule"
- (Parse_Spec.opt_thm_name ":" -- Parse.xthm --
+ (Parse_Spec.opt_thm_name ":" -- Parse.thm --
Scan.optional parse_splits [] >> simps_of_case_cmd)
end
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Apr 13 14:12:51 2016 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Apr 13 18:04:27 2016 +0200
@@ -536,7 +536,7 @@
let
val ref_of_str = (* FIXME proper wrapper for parser combinators *)
suffix ";" #> Token.explode (Thy_Header.get_keywords' ctxt) Position.none
- #> Parse.xthm #> fst
+ #> Parse.thm #> fst
val thms = named_thms |> maps snd
val facts = named_thms |> map (ref_of_str o fst o fst)
val fact_override = {add = facts, del = [], only = true}
--- a/src/HOL/Nominal/nominal_inductive.ML Wed Apr 13 14:12:51 2016 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML Wed Apr 13 18:04:27 2016 +0200
@@ -680,14 +680,14 @@
val _ =
Outer_Syntax.local_theory_to_proof @{command_keyword nominal_inductive}
"prove equivariance and strong induction theorem for inductive predicate involving nominal datatypes"
- (Parse.xname -- Scan.optional (@{keyword "avoids"} |-- Parse.and_list1 (Parse.name --
+ (Parse.name -- Scan.optional (@{keyword "avoids"} |-- Parse.and_list1 (Parse.name --
(@{keyword ":"} |-- Scan.repeat1 Parse.name))) [] >> (fn (name, avoids) =>
prove_strong_ind name avoids));
val _ =
Outer_Syntax.local_theory @{command_keyword equivariance}
"prove equivariance for inductive predicate involving nominal datatypes"
- (Parse.xname -- Scan.optional (@{keyword "["} |-- Parse.list1 Parse.name --| @{keyword "]"}) [] >>
+ (Parse.name -- Scan.optional (@{keyword "["} |-- Parse.list1 Parse.name --| @{keyword "]"}) [] >>
(fn (name, atoms) => prove_eqvt name atoms));
end
--- a/src/HOL/Nominal/nominal_inductive2.ML Wed Apr 13 14:12:51 2016 +0200
+++ b/src/HOL/Nominal/nominal_inductive2.ML Wed Apr 13 18:04:27 2016 +0200
@@ -488,7 +488,7 @@
val _ =
Outer_Syntax.local_theory_to_proof @{command_keyword nominal_inductive2}
"prove strong induction theorem for inductive predicate involving nominal datatypes"
- (Parse.xname --
+ (Parse.name --
Scan.option (@{keyword "("} |-- Parse.!!! (Parse.name --| @{keyword ")"})) --
(Scan.optional (@{keyword "avoids"} |-- Parse.enum1 "|" (Parse.name --
(@{keyword ":"} |-- Parse.and_list1 Parse.term))) []) >> (fn ((name, rule_name), avoids) =>
--- a/src/HOL/SPARK/Manual/Reference.thy Wed Apr 13 14:12:51 2016 +0200
+++ b/src/HOL/SPARK/Manual/Reference.thy Wed Apr 13 18:04:27 2016 +0200
@@ -51,7 +51,7 @@
@{rail \<open>
@'spark_types' ((name '=' type (mapping?))+)
;
- mapping: '('((name '=' nameref)+',')')'
+ mapping: '('((name '=' name)+',')')'
\<close>}
Associates a \SPARK{} type with the given name with an Isabelle type. This command can
only be used outside a verification environment. The given type must be either a record
--- a/src/HOL/SPARK/Tools/spark_commands.ML Wed Apr 13 14:12:51 2016 +0200
+++ b/src/HOL/SPARK/Tools/spark_commands.ML Wed Apr 13 18:04:27 2016 +0200
@@ -117,7 +117,7 @@
"associate SPARK types with types"
(Scan.repeat1 (Parse.name -- Parse.!!! (Args.$$$ "=" |-- Parse.typ --
Scan.optional (Args.parens (Parse.list1
- (Parse.name -- Parse.!!! (Args.$$$ "=" |-- Parse.xname)))) [])) >>
+ (Parse.name -- Parse.!!! (Args.$$$ "=" |-- Parse.name)))) [])) >>
(Toplevel.theory o fold add_spark_type_cmd));
val _ =
--- a/src/HOL/Statespace/state_space.ML Wed Apr 13 14:12:51 2016 +0200
+++ b/src/HOL/Statespace/state_space.ML Wed Apr 13 18:04:27 2016 +0200
@@ -642,7 +642,7 @@
val parent =
Parse_Spec.locale_prefix --
- ((type_insts -- Parse.xname) || (Parse.xname >> pair [])) -- renames
+ ((type_insts -- Parse.name) || (Parse.name >> pair [])) -- renames
>> (fn ((prefix, (insts, name)), renames) => (prefix, (insts, name, renames)));
in
--- a/src/HOL/Tools/BNF/bnf_lift.ML Wed Apr 13 14:12:51 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_lift.ML Wed Apr 13 18:04:27 2016 +0200
@@ -426,7 +426,7 @@
Scan.optional (@{keyword "("} |-- Plugin_Name.parse_filter --| @{keyword ")"})
(K Plugin_Name.default_filter) >> Plugins_Option >> single;
-val parse_typedef_thm = Scan.option (Parse.reserved "via" |-- Parse.xthm);
+val parse_typedef_thm = Scan.option (Parse.reserved "via" |-- Parse.thm);
in
--- a/src/HOL/Tools/Function/partial_function.ML Wed Apr 13 14:12:51 2016 +0200
+++ b/src/HOL/Tools/Function/partial_function.ML Wed Apr 13 18:04:27 2016 +0200
@@ -305,7 +305,7 @@
val add_partial_function = gen_add_partial_function Specification.check_spec;
val add_partial_function_cmd = gen_add_partial_function Specification.read_spec;
-val mode = @{keyword "("} |-- Parse.xname --| @{keyword ")"};
+val mode = @{keyword "("} |-- Parse.name --| @{keyword ")"};
val _ =
Outer_Syntax.local_theory @{command_keyword partial_function} "define partial function"
--- a/src/HOL/Tools/Lifting/lifting_def_code_dt.ML Wed Apr 13 14:12:51 2016 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def_code_dt.ML Wed Apr 13 18:04:27 2016 +0200
@@ -812,7 +812,7 @@
(((Parse.binding -- (@{keyword "::"} |-- (Parse.typ >> SOME) -- Parse.opt_mixfix')
>> Scan.triple2) --
(@{keyword "is"} |-- Parse.term) --
- Scan.optional (@{keyword "parametric"} |-- Parse.!!! Parse.xthms1) []) >> Scan.triple1)
+ Scan.optional (@{keyword "parametric"} |-- Parse.!!! Parse.thms1) []) >> Scan.triple1)
>> lift_def_cmd_with_err_handling);
end
--- a/src/HOL/Tools/Lifting/lifting_setup.ML Wed Apr 13 14:12:51 2016 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML Wed Apr 13 18:04:27 2016 +0200
@@ -809,8 +809,8 @@
val _ =
Outer_Syntax.local_theory @{command_keyword setup_lifting}
"setup lifting infrastructure"
- (Parse.xthm -- Scan.option Parse.xthm
- -- Scan.option (@{keyword "parametric"} |-- Parse.!!! Parse.xthm) >>
+ (Parse.thm -- Scan.option Parse.thm
+ -- Scan.option (@{keyword "parametric"} |-- Parse.!!! Parse.thm) >>
(fn ((xthm, opt_reflp_xthm), opt_par_xthm) =>
setup_lifting_cmd xthm opt_reflp_xthm opt_par_xthm))
@@ -1024,7 +1024,7 @@
val _ =
Outer_Syntax.local_theory @{command_keyword lifting_forget}
"unsetup Lifting and Transfer for the given lifting bundle"
- (Parse.position Parse.xname >> (lifting_forget_cmd))
+ (Parse.position Parse.name >> (lifting_forget_cmd))
(* lifting_update *)
@@ -1053,6 +1053,6 @@
val _ =
Outer_Syntax.local_theory @{command_keyword lifting_update}
"add newly introduced transfer rules to a bundle storing the state of Lifting and Transfer"
- (Parse.position Parse.xname >> lifting_update_cmd)
+ (Parse.position Parse.name >> lifting_update_cmd)
end
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Wed Apr 13 14:12:51 2016 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Wed Apr 13 18:04:27 2016 +0200
@@ -1030,7 +1030,7 @@
(* values command for Prolog queries *)
val opt_print_modes =
- Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) []
+ Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.name --| @{keyword ")"})) []
val _ =
Outer_Syntax.command @{command_keyword values_prolog}
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Wed Apr 13 14:12:51 2016 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Wed Apr 13 18:04:27 2016 +0200
@@ -222,12 +222,12 @@
parse_mode_tuple_expr) xs
val mode_and_opt_proposal = parse_mode_expr --
- Scan.optional (Args.$$$ "as" |-- Parse.xname >> SOME) NONE
+ Scan.optional (Args.$$$ "as" |-- Parse.name >> SOME) NONE
val opt_modes =
Scan.optional (@{keyword "("} |-- Args.$$$ "modes" |-- @{keyword ":"} |--
- (((Parse.enum1 "and" (Parse.xname --| @{keyword ":"} --
+ (((Parse.enum1 "and" (Parse.name --| @{keyword ":"} --
(Parse.enum "," mode_and_opt_proposal))) >> Multiple_Preds)
|| ((Parse.enum "," mode_and_opt_proposal) >> Single_Pred))
--| @{keyword ")"}) (Multiple_Preds [])
@@ -250,7 +250,7 @@
end
val opt_print_modes =
- Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) []
+ Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.name --| @{keyword ")"})) []
val opt_mode = (Args.$$$ "_" >> K NONE) || (parse_mode_expr >> SOME)
--- a/src/HOL/Tools/Quotient/quotient_type.ML Wed Apr 13 14:12:51 2016 +0200
+++ b/src/HOL/Tools/Quotient/quotient_type.ML Wed Apr 13 18:04:27 2016 +0200
@@ -348,7 +348,7 @@
Parse.opt_mixfix -- (@{keyword "="} |-- Parse.typ) -- (@{keyword "/"} |--
Scan.optional (Parse.reserved "partial" -- @{keyword ":"} >> K true) false -- Parse.term) --
Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding)) --
- Scan.option (@{keyword "parametric"} |-- Parse.!!! Parse.xthm))
+ Scan.option (@{keyword "parametric"} |-- Parse.!!! Parse.thm))
>> (fn (overloaded, spec) => quotient_type_cmd {overloaded = overloaded} spec))
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Wed Apr 13 14:12:51 2016 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Wed Apr 13 18:04:27 2016 +0200
@@ -349,10 +349,10 @@
val parse_query_bang = @{keyword "?"} || @{keyword "!"} || @{keyword "!!"}
val parse_key = Scan.repeat1 (Parse.typ_group || parse_query_bang) >> implode_param
-val parse_value = Scan.repeat1 (Parse.xname || Parse.float_number || parse_query_bang)
+val parse_value = Scan.repeat1 (Parse.name || Parse.float_number || parse_query_bang)
val parse_param = parse_key -- Scan.optional (@{keyword "="} |-- parse_value) []
val parse_params = Scan.optional (Args.bracks (Parse.list parse_param)) []
-val parse_fact_refs = Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) Parse.xthm)
+val parse_fact_refs = Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) Parse.thm)
val parse_fact_override_chunk =
(Args.add |-- Args.colon |-- parse_fact_refs >> add_fact_override)
|| (Args.del |-- Args.colon |-- parse_fact_refs >> del_fact_override)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Wed Apr 13 14:12:51 2016 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Wed Apr 13 18:04:27 2016 +0200
@@ -129,7 +129,7 @@
|> Symbol.source
|> Token.source keywords Position.start
|> Token.source_proper
- |> Source.source Token.stopper (Parse.xthms1 >> get)
+ |> Source.source Token.stopper (Parse.thms1 >> get)
|> Source.exhaust
end
--- a/src/HOL/Tools/inductive.ML Wed Apr 13 14:12:51 2016 +0200
+++ b/src/HOL/Tools/inductive.ML Wed Apr 13 18:04:27 2016 +0200
@@ -1182,7 +1182,7 @@
fun gen_ind_decl mk_def coind =
Parse.fixes -- Parse.for_fixes --
Scan.optional Parse_Spec.where_alt_specs [] --
- Scan.optional (@{keyword "monos"} |-- Parse.!!! Parse.xthms1) []
+ Scan.optional (@{keyword "monos"} |-- Parse.!!! Parse.thms1) []
>> (fn (((preds, params), specs), monos) =>
(snd o gen_add_inductive mk_def true coind preds params specs monos));
--- a/src/HOL/Tools/record.ML Wed Apr 13 14:12:51 2016 +0200
+++ b/src/HOL/Tools/record.ML Wed Apr 13 18:04:27 2016 +0200
@@ -2411,7 +2411,7 @@
Toplevel.theory (add_record_cmd {overloaded = overloaded} x y z)));
val opt_modes =
- Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) []
+ Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.name --| @{keyword ")"})) []
val _ =
Outer_Syntax.command @{command_keyword "print_record"} "print record definiton"
--- a/src/HOL/Tools/try0.ML Wed Apr 13 14:12:51 2016 +0200
+++ b/src/HOL/Tools/try0.ML Wed Apr 13 18:04:27 2016 +0200
@@ -166,7 +166,7 @@
implode (map (enclose "[" "]" o Pretty.unformatted_string_of o Token.pretty_src @{context}) args);
val parse_fact_refs =
- Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) (Parse.xthm >> string_of_xthm));
+ Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) (Parse.thm >> string_of_xthm));
val parse_attr =
Args.$$$ "simp" |-- Args.colon |-- parse_fact_refs >> (fn ss => (ss, [], [], []))
--- a/src/HOL/Tools/value.ML Wed Apr 13 14:12:51 2016 +0200
+++ b/src/HOL/Tools/value.ML Wed Apr 13 18:04:27 2016 +0200
@@ -64,10 +64,10 @@
in Pretty.writeln p end;
val opt_modes =
- Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) [];
+ Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.name --| @{keyword ")"})) [];
val opt_evaluator =
- Scan.option (@{keyword "["} |-- Parse.xname --| @{keyword "]"})
+ Scan.option (@{keyword "["} |-- Parse.name --| @{keyword "]"})
val _ =
Outer_Syntax.command @{command_keyword value} "evaluate and print term"
--- a/src/Pure/General/name_space.ML Wed Apr 13 14:12:51 2016 +0200
+++ b/src/Pure/General/name_space.ML Wed Apr 13 18:04:27 2016 +0200
@@ -251,11 +251,14 @@
fun completion context space (xname, pos) =
Completion.make (xname, pos) (fn completed =>
let
- fun result_ord ((xname1, (_, name1)), (xname2, (_, name2))) =
- (case bool_ord (apply2 (is_some o Long_Name.dest_local) (name2, name1)) of
+ fun result_ord ((precise1, (xname1, (_, name1))), (precise2, (xname2, (_, name2)))) =
+ (case bool_ord (precise2, precise1) of
EQUAL =>
- (case int_ord (apply2 Long_Name.qualification (xname1, xname2)) of
- EQUAL => string_ord (xname1, xname2)
+ (case bool_ord (apply2 (is_some o Long_Name.dest_local) (name2, name1)) of
+ EQUAL =>
+ (case int_ord (apply2 Long_Name.qualification (xname1, xname2)) of
+ EQUAL => string_ord (xname1, xname2)
+ | ord => ord)
| ord => ord)
| ord => ord);
val Name_Space {kind, internals, ...} = space;
@@ -264,11 +267,11 @@
Change_Table.fold
(fn (a, (name :: _, _)) =>
if completed a andalso not (is_concealed space name) then
- let val a' = ext name
- in if a = a' then cons (a', (kind, name)) else I end
+ cons (a = ext name, (a, (kind, name)))
else I
| _ => I) internals []
|> sort_distinct result_ord
+ |> map #2
end);
--- a/src/Pure/Isar/method.ML Wed Apr 13 14:12:51 2016 +0200
+++ b/src/Pure/Isar/method.ML Wed Apr 13 18:04:27 2016 +0200
@@ -599,7 +599,7 @@
local
fun sect (modifier : modifier parser) = Scan.depend (fn context =>
- Scan.ahead Parse.not_eof -- Scan.trace modifier -- Scan.repeat (Scan.unless modifier Parse.xthm)
+ Scan.ahead Parse.not_eof -- Scan.trace modifier -- Scan.repeat (Scan.unless modifier Parse.thm)
>> (fn ((tok0, ({init, attribute, pos}, modifier_toks)), xthms) =>
let
val decl =
@@ -689,7 +689,7 @@
fun parser pri =
let
- val meth_name = Parse.token Parse.xname;
+ val meth_name = Parse.token Parse.name;
fun meth5 x =
(meth_name >> (Source o single) ||
--- a/src/Pure/Isar/parse.ML Wed Apr 13 14:12:51 2016 +0200
+++ b/src/Pure/Isar/parse.ML Wed Apr 13 18:04:27 2016 +0200
@@ -64,12 +64,10 @@
val properties: Properties.T parser
val name: bstring parser
val binding: binding parser
- val xname: xstring parser
val text: string parser
val path: string parser
- val theory_name: bstring parser
- val theory_xname: xstring parser
- val liberal_name: xstring parser
+ val theory_name: string parser
+ val liberal_name: string parser
val parname: string parser
val parbinding: binding parser
val class: string parser
@@ -104,15 +102,15 @@
val termp: (string * string list) parser
val private: Position.T parser
val qualified: Position.T parser
- val target: (xstring * Position.T) parser
- val opt_target: (xstring * Position.T) option parser
+ val target: (string * Position.T) parser
+ val opt_target: (string * Position.T) option parser
val args: Token.T list parser
val args1: (string -> bool) -> Token.T list parser
val attribs: Token.src list parser
val opt_attribs: Token.src list parser
val thm_sel: Facts.interval list parser
- val xthm: (Facts.ref * Token.src list) parser
- val xthms1: (Facts.ref * Token.src list) list parser
+ val thm: (Facts.ref * Token.src list) parser
+ val thms1: (Facts.ref * Token.src list) list parser
end;
structure Parse: PARSE =
@@ -261,22 +259,20 @@
(* names and text *)
-val name = group (fn () => "name declaration") (short_ident || sym_ident || string || number);
+val name =
+ group (fn () => "name") (short_ident || long_ident || sym_ident || string || number);
val binding = position name >> Binding.make;
-val xname = group (fn () => "name reference")
- (short_ident || long_ident || sym_ident || string || number);
-
-val text = group (fn () => "text")
- (short_ident || long_ident || sym_ident || string || number || verbatim || cartouche);
+val text =
+ group (fn () => "text")
+ (short_ident || long_ident || sym_ident || string || number || verbatim || cartouche);
val path = group (fn () => "file name/path specification") name;
val theory_name = group (fn () => "theory name") name;
-val theory_xname = group (fn () => "theory name reference") xname;
-val liberal_name = keyword_with Token.ident_or_symbolic || xname;
+val liberal_name = keyword_with Token.ident_or_symbolic || name;
val parname = Scan.optional ($$$ "(" |-- name --| $$$ ")") "";
val parbinding = Scan.optional ($$$ "(" |-- binding --| $$$ ")") Binding.empty;
@@ -284,11 +280,11 @@
(* type classes *)
-val class = group (fn () => "type class") (inner_syntax xname);
+val class = group (fn () => "type class") (inner_syntax name);
-val sort = group (fn () => "sort") (inner_syntax xname);
+val sort = group (fn () => "sort") (inner_syntax name);
-val type_const = inner_syntax (group (fn () => "type constructor") xname);
+val type_const = inner_syntax (group (fn () => "type constructor") name);
val arity = type_const -- ($$$ "::" |-- !!!
(Scan.optional ($$$ "(" |-- !!! (list1 sort --| $$$ ")")) [] -- sort)) >> Scan.triple2;
@@ -398,7 +394,7 @@
val term = inner_syntax term_group;
val prop = inner_syntax prop_group;
-val const = inner_syntax (group (fn () => "constant") xname);
+val const = inner_syntax (group (fn () => "constant") name);
val literal_fact = inner_syntax (group (fn () => "literal fact") (alt_string || cartouche));
@@ -417,7 +413,7 @@
val private = position ($$$ "private") >> #2;
val qualified = position ($$$ "qualified") >> #2;
-val target = ($$$ "(" -- $$$ "in") |-- !!! (position xname --| $$$ ")");
+val target = ($$$ "(" -- $$$ "in") |-- !!! (position name --| $$$ ")");
val opt_target = Scan.option target;
@@ -468,11 +464,11 @@
nat --| minus >> Facts.From ||
nat >> Facts.Single) --| $$$ ")";
-val xthm =
+val thm =
$$$ "[" |-- attribs --| $$$ "]" >> pair (Facts.named "") ||
(literal_fact >> Facts.Fact ||
- position xname -- Scan.option thm_sel >> Facts.Named) -- opt_attribs;
+ position name -- Scan.option thm_sel >> Facts.Named) -- opt_attribs;
-val xthms1 = Scan.repeat1 xthm;
+val thms1 = Scan.repeat1 thm;
end;
--- a/src/Pure/Isar/parse.scala Wed Apr 13 14:12:51 2016 +0200
+++ b/src/Pure/Isar/parse.scala Wed Apr 13 18:04:27 2016 +0200
@@ -67,8 +67,7 @@
def string: Parser[String] = atom("string", _.is_string)
def nat: Parser[Int] = atom("natural number", _.is_nat) ^^ (s => Integer.parseInt(s))
- def name: Parser[String] = atom("name declaration", _.is_name)
- def xname: Parser[String] = atom("name reference", _.is_xname)
+ def name: Parser[String] = atom("name", _.is_name)
def text: Parser[String] = atom("text", _.is_text)
def ML_source: Parser[String] = atom("ML source", _.is_text)
def document_source: Parser[String] = atom("document source", _.is_text)
@@ -78,8 +77,6 @@
def theory_name: Parser[String] =
atom("theory name", tok => tok.is_name && Path.is_wellformed(tok.content))
- def theory_xname: Parser[String] =
- atom("theory name reference", tok => tok.is_xname && Path.is_wellformed(tok.content))
private def tag_name: Parser[String] =
atom("tag name", tok =>
--- a/src/Pure/Isar/parse_spec.ML Wed Apr 13 14:12:51 2016 +0200
+++ b/src/Pure/Isar/parse_spec.ML Wed Apr 13 18:04:27 2016 +0200
@@ -55,7 +55,7 @@
val where_alt_specs = Parse.where_ |-- Parse.!!! alt_specs;
-val name_facts = Parse.and_list1 (opt_thm_name "=" -- Parse.xthms1);
+val name_facts = Parse.and_list1 (opt_thm_name "=" -- Parse.thms1);
(* basic constant specifications *)
@@ -72,7 +72,7 @@
(* locale and context elements *)
-val includes = Parse.$$$ "includes" |-- Parse.!!! (Scan.repeat1 (Parse.position Parse.xname));
+val includes = Parse.$$$ "includes" |-- Parse.!!! (Scan.repeat1 (Parse.position Parse.name));
val locale_fixes =
Parse.and_list1 (Parse.binding -- Scan.option (Parse.$$$ "::" |-- Parse.typ) -- Parse.mixfix
@@ -95,7 +95,7 @@
>> Element.Assumes ||
Parse.$$$ "defines" |-- Parse.!!! (Parse.and_list1 (opt_thm_name ":" -- Parse.propp))
>> Element.Defines ||
- Parse.$$$ "notes" |-- Parse.!!! (Parse.and_list1 (opt_thm_name "=" -- Parse.xthms1))
+ Parse.$$$ "notes" |-- Parse.!!! (Parse.and_list1 (opt_thm_name "=" -- Parse.thms1))
>> (curry Element.Notes "");
fun plus1_unless test scan =
@@ -120,7 +120,7 @@
val locale_expression =
let
- val expr2 = Parse.position Parse.xname;
+ val expr2 = Parse.position Parse.name;
val expr1 =
locale_prefix -- expr2 --
Scan.optional instance (Expression.Named []) >> (fn ((p, l), i) => (l, (p, i)));
--- a/src/Pure/Isar/token.ML Wed Apr 13 14:12:51 2016 +0200
+++ b/src/Pure/Isar/token.ML Wed Apr 13 18:04:27 2016 +0200
@@ -38,7 +38,6 @@
val kind_of: T -> kind
val is_kind: kind -> T -> bool
val is_command: T -> bool
- val is_name: T -> bool
val keyword_with: (string -> bool) -> T -> bool
val is_command_modifier: T -> bool
val ident_with: (string -> bool) -> T -> bool
@@ -210,8 +209,6 @@
val is_command = is_kind Command;
-val is_name = is_kind Ident orf is_kind Sym_Ident orf is_kind String orf is_kind Nat;
-
fun keyword_with pred (Token (_, (Keyword, x), _)) = pred x
| keyword_with _ _ = false;
--- a/src/Pure/Isar/token.scala Wed Apr 13 14:12:51 2016 +0200
+++ b/src/Pure/Isar/token.scala Wed Apr 13 18:04:27 2016 +0200
@@ -236,11 +236,11 @@
def is_float: Boolean = kind == Token.Kind.FLOAT
def is_name: Boolean =
kind == Token.Kind.IDENT ||
+ kind == Token.Kind.LONG_IDENT ||
kind == Token.Kind.SYM_IDENT ||
kind == Token.Kind.STRING ||
kind == Token.Kind.NAT
- def is_xname: Boolean = is_name || kind == Token.Kind.LONG_IDENT
- def is_text: Boolean = is_xname || kind == Token.Kind.VERBATIM || kind == Token.Kind.CARTOUCHE
+ def is_text: Boolean = is_name || kind == Token.Kind.VERBATIM || kind == Token.Kind.CARTOUCHE
def is_space: Boolean = kind == Token.Kind.SPACE
def is_comment: Boolean = kind == Token.Kind.COMMENT
def is_improper: Boolean = is_space || is_comment
--- a/src/Pure/ML/ml_context.ML Wed Apr 13 14:12:51 2016 +0200
+++ b/src/Pure/ML/ml_context.ML Wed Apr 13 18:04:27 2016 +0200
@@ -96,7 +96,7 @@
local
val antiq =
- Parse.!!! ((Parse.token Parse.xname ::: Parse.args) --| Scan.ahead Parse.eof);
+ Parse.!!! ((Parse.token Parse.name ::: Parse.args) --| Scan.ahead Parse.eof);
fun make_env name visible =
(ML_Lex.tokenize
--- a/src/Pure/Pure.thy Wed Apr 13 14:12:51 2016 +0200
+++ b/src/Pure/Pure.thy Wed Apr 13 18:04:27 2016 +0200
@@ -280,7 +280,7 @@
val trans_pat =
Scan.optional
- (@{keyword "("} |-- Parse.!!! (Parse.inner_syntax Parse.xname --| @{keyword ")"})) "logic"
+ (@{keyword "("} |-- Parse.!!! (Parse.inner_syntax Parse.name --| @{keyword ")"})) "logic"
-- Parse.inner_syntax Parse.string;
fun trans_arrow toks =
@@ -403,7 +403,7 @@
val _ =
Outer_Syntax.local_theory' @{command_keyword declare} "declare theorems"
- (Parse.and_list1 Parse.xthms1 -- Parse.for_fixes
+ (Parse.and_list1 Parse.thms1 -- Parse.for_fixes
>> (fn (facts, fixes) =>
#2 oo Specification.theorems_cmd "" [(Attrib.empty_binding, flat facts)] fixes));
@@ -442,7 +442,7 @@
val _ =
hide_names @{command_keyword hide_fact} "facts" Global_Theory.hide_fact
- (Parse.position Parse.xname) (Global_Theory.check_fact o Proof_Context.theory_of);
+ (Parse.position Parse.name) (Global_Theory.check_fact o Proof_Context.theory_of);
in end\<close>
@@ -454,18 +454,18 @@
val _ =
Outer_Syntax.local_theory @{command_keyword bundle} "define bundle of declarations"
- ((Parse.binding --| @{keyword "="}) -- Parse.xthms1 -- Parse.for_fixes
+ ((Parse.binding --| @{keyword "="}) -- Parse.thms1 -- Parse.for_fixes
>> (uncurry Bundle.bundle_cmd));
val _ =
Outer_Syntax.command @{command_keyword include}
"include declarations from bundle in proof body"
- (Scan.repeat1 (Parse.position Parse.xname) >> (Toplevel.proof o Bundle.include_cmd));
+ (Scan.repeat1 (Parse.position Parse.name) >> (Toplevel.proof o Bundle.include_cmd));
val _ =
Outer_Syntax.command @{command_keyword including}
"include declarations from bundle in goal refinement"
- (Scan.repeat1 (Parse.position Parse.xname) >> (Toplevel.proof o Bundle.including_cmd));
+ (Scan.repeat1 (Parse.position Parse.name) >> (Toplevel.proof o Bundle.including_cmd));
val _ =
Outer_Syntax.command @{command_keyword print_bundles}
@@ -484,7 +484,7 @@
val _ =
Outer_Syntax.command @{command_keyword context} "begin local theory context"
- ((Parse.position Parse.xname >> (fn name =>
+ ((Parse.position Parse.name >> (fn name =>
Toplevel.begin_local_theory true (Named_Target.begin name)) ||
Scan.optional Parse_Spec.includes [] -- Scan.repeat Parse_Spec.context_element
>> (fn (incls, elems) => Toplevel.open_target (#2 o Bundle.context_cmd incls elems)))
@@ -550,7 +550,7 @@
val _ =
Outer_Syntax.command @{command_keyword sublocale}
"prove sublocale relation between a locale and a locale expression"
- ((Parse.position Parse.xname --| (@{keyword "\<subseteq>"} || @{keyword "<"}) --
+ ((Parse.position Parse.name --| (@{keyword "\<subseteq>"} || @{keyword "<"}) --
interpretation_args_with_defs >> (fn (loc, (expr, (defs, equations))) =>
Toplevel.theory_to_proof (Interpretation.global_sublocale_cmd loc expr defs equations)))
|| interpretation_args_with_defs >> (fn (expr, (defs, equations)) =>
@@ -684,7 +684,7 @@
ML \<open>
local
-val facts = Parse.and_list1 Parse.xthms1;
+val facts = Parse.and_list1 Parse.thms1;
val _ =
Outer_Syntax.command @{command_keyword then} "forward chaining"
@@ -773,9 +773,9 @@
Outer_Syntax.command @{command_keyword case} "invoke local context"
(Parse_Spec.opt_thm_name ":" --
(@{keyword "("} |--
- Parse.!!! (Parse.position Parse.xname -- Scan.repeat (Parse.maybe Parse.binding)
+ Parse.!!! (Parse.position Parse.name -- Scan.repeat (Parse.maybe Parse.binding)
--| @{keyword ")"}) ||
- Parse.position Parse.xname >> rpair []) >> (Toplevel.proof o Proof.case_cmd));
+ Parse.position Parse.name >> rpair []) >> (Toplevel.proof o Proof.case_cmd));
in end\<close>
@@ -906,7 +906,7 @@
local
val calculation_args =
- Scan.option (@{keyword "("} |-- Parse.!!! ((Parse.xthms1 --| @{keyword ")"})));
+ Scan.option (@{keyword "("} |-- Parse.!!! ((Parse.thms1 --| @{keyword ")"})));
val _ =
Outer_Syntax.command @{command_keyword also} "combine calculation and current facts"
@@ -956,7 +956,7 @@
local
val opt_modes =
- Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) [];
+ Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.name --| @{keyword ")"})) [];
val _ =
Outer_Syntax.command @{command_keyword help}
@@ -1025,13 +1025,13 @@
val _ =
Outer_Syntax.command @{command_keyword print_locale}
"print locale of this theory"
- (Parse.opt_bang -- Parse.position Parse.xname >> (fn (b, name) =>
+ (Parse.opt_bang -- Parse.position Parse.name >> (fn (b, name) =>
Toplevel.keep (fn state => Locale.print_locale (Toplevel.theory_of state) b name)));
val _ =
Outer_Syntax.command @{command_keyword print_interps}
"print interpretations of locale for this theory or proof context"
- (Parse.position Parse.xname >> (fn name =>
+ (Parse.position Parse.name >> (fn name =>
Toplevel.keep (fn state => Locale.print_registrations (Toplevel.context_of state) name)));
val _ =
@@ -1100,19 +1100,19 @@
val _ =
Outer_Syntax.command @{command_keyword print_statement}
"print theorems as long statements"
- (opt_modes -- Parse.xthms1 >> Isar_Cmd.print_stmts);
+ (opt_modes -- Parse.thms1 >> Isar_Cmd.print_stmts);
val _ =
Outer_Syntax.command @{command_keyword thm} "print theorems"
- (opt_modes -- Parse.xthms1 >> Isar_Cmd.print_thms);
+ (opt_modes -- Parse.thms1 >> Isar_Cmd.print_thms);
val _ =
Outer_Syntax.command @{command_keyword prf} "print proof terms of theorems"
- (opt_modes -- Scan.option Parse.xthms1 >> Isar_Cmd.print_prfs false);
+ (opt_modes -- Scan.option Parse.thms1 >> Isar_Cmd.print_prfs false);
val _ =
Outer_Syntax.command @{command_keyword full_prf} "print full proof terms of theorems"
- (opt_modes -- Scan.option Parse.xthms1 >> Isar_Cmd.print_prfs true);
+ (opt_modes -- Scan.option Parse.thms1 >> Isar_Cmd.print_prfs true);
val _ =
Outer_Syntax.command @{command_keyword prop} "read and print proposition"
@@ -1156,8 +1156,8 @@
local
val theory_bounds =
- Parse.position Parse.theory_xname >> single ||
- (@{keyword "("} |-- Parse.enum "|" (Parse.position Parse.theory_xname) --| @{keyword ")"});
+ Parse.position Parse.theory_name >> single ||
+ (@{keyword "("} |-- Parse.enum "|" (Parse.position Parse.theory_name) --| @{keyword ")"});
val _ =
Outer_Syntax.command @{command_keyword thy_deps} "visualize theory dependencies"
@@ -1177,14 +1177,14 @@
val _ =
Outer_Syntax.command @{command_keyword thm_deps} "visualize theorem dependencies"
- (Parse.xthms1 >> (fn args =>
+ (Parse.thms1 >> (fn args =>
Toplevel.keep (fn st =>
Thm_Deps.thm_deps (Toplevel.theory_of st)
(Attrib.eval_thms (Toplevel.context_of st) args))));
val thy_names =
- Scan.repeat1 (Scan.unless Parse.minus (Parse.position Parse.theory_xname));
+ Scan.repeat1 (Scan.unless Parse.minus (Parse.position Parse.theory_name));
val _ =
Outer_Syntax.command @{command_keyword unused_thms} "find unused theorems"
@@ -1260,7 +1260,7 @@
val _ =
Outer_Syntax.command @{command_keyword realizers}
"specify realizers for primitive axioms / theorems, together with correctness proof"
- (Scan.repeat1 (Parse.xname -- parse_vars --| Parse.$$$ ":" -- Parse.string -- Parse.string) >>
+ (Scan.repeat1 (Parse.name -- parse_vars --| Parse.$$$ ":" -- Parse.string -- Parse.string) >>
(fn xs => Toplevel.theory (fn thy => Extraction.add_realizers
(map (fn (((a, vs), s1), s2) => (Global_Theory.get_thm thy a, (vs, s1, s2))) xs) thy)));
@@ -1276,7 +1276,7 @@
val _ =
Outer_Syntax.command @{command_keyword extract} "extract terms from proofs"
- (Scan.repeat1 (Parse.xname -- parse_vars) >> (fn xs => Toplevel.theory (fn thy =>
+ (Scan.repeat1 (Parse.name -- parse_vars) >> (fn xs => Toplevel.theory (fn thy =>
Extraction.extract (map (apfst (Global_Theory.get_thm thy)) xs) thy)));
in end\<close>
--- a/src/Pure/System/options.scala Wed Apr 13 14:12:51 2016 +0200
+++ b/src/Pure/System/options.scala Wed Apr 13 18:04:27 2016 +0200
@@ -80,15 +80,18 @@
lazy val prefs_syntax = Outer_Syntax.init() + "="
- object Parser extends Parse.Parser
+ trait Parser extends Parse.Parser
{
- val option_name = atom("option name", _.is_xname)
- val option_type = atom("option type", _.is_ident)
+ val option_name = atom("option name", _.is_name)
+ val option_type = atom("option type", _.is_name)
val option_value =
opt(token("-", tok => tok.is_sym_ident && tok.content == "-")) ~ atom("nat", _.is_nat) ^^
{ case s ~ n => if (s.isDefined) "-" + n else n } |
atom("option value", tok => tok.is_name || tok.is_float)
+ }
+ object Parser extends Parse.Parser with Parser
+ {
def comment_marker: Parser[String] =
$$$("--") | $$$(Symbol.comment) | $$$(Symbol.comment_decoded)
--- a/src/Pure/Thy/sessions.scala Wed Apr 13 14:12:51 2016 +0200
+++ b/src/Pure/Thy/sessions.scala Wed Apr 13 18:04:27 2016 +0200
@@ -167,7 +167,7 @@
(CHAPTER, Keyword.THY_DECL) + (SESSION, Keyword.THY_DECL) +
IN + DESCRIPTION + OPTIONS + GLOBAL_THEORIES + THEORIES + FILES + DOCUMENT_FILES
- private object Parser extends Parse.Parser
+ private object Parser extends Parse.Parser with Options.Parser
{
private abstract class Entry
private sealed case class Chapter(name: String) extends Entry
@@ -195,12 +195,13 @@
val session_name = atom("session name", _.is_name)
val option =
- name ~ opt($$$("=") ~! name ^^ { case _ ~ x => x }) ^^ { case x ~ y => (x, y) }
+ option_name ~ opt($$$("=") ~! option_value ^^
+ { case _ ~ x => x }) ^^ { case x ~ y => (x, y) }
val options = $$$("[") ~> rep1sep(option, $$$(",")) <~ $$$("]")
val theories =
($$$(GLOBAL_THEORIES) | $$$(THEORIES)) ~!
- ((options | success(Nil)) ~ rep(theory_xname)) ^^
+ ((options | success(Nil)) ~ rep(theory_name)) ^^
{ case x ~ (y ~ z) => (x == GLOBAL_THEORIES, y, z) }
val document_files =
--- a/src/Pure/Thy/term_style.ML Wed Apr 13 14:12:51 2016 +0200
+++ b/src/Pure/Thy/term_style.ML Wed Apr 13 18:04:27 2016 +0200
@@ -32,7 +32,7 @@
(* style parsing *)
fun parse_single ctxt =
- Parse.token Parse.xname ::: Parse.args >> (fn src0 =>
+ Parse.token Parse.name ::: Parse.args >> (fn src0 =>
let
val (src, parse) = Token.check_src ctxt get_data src0;
val (f, _) = Token.syntax (Scan.lift parse) src ctxt;
--- a/src/Pure/Thy/thy_header.ML Wed Apr 13 14:12:51 2016 +0200
+++ b/src/Pure/Thy/thy_header.ML Wed Apr 13 18:04:27 2016 +0200
@@ -117,7 +117,7 @@
fun imports name =
if name = Context.PureN then Scan.succeed []
- else Parse.$$$ importsN |-- Parse.!!! (Scan.repeat1 (Parse.position Parse.theory_xname));
+ else Parse.$$$ importsN |-- Parse.!!! (Scan.repeat1 (Parse.position Parse.theory_name));
val opt_files =
Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.list1 Parse.name) --| Parse.$$$ ")") [];
--- a/src/Pure/Thy/thy_header.scala Wed Apr 13 14:12:51 2016 +0200
+++ b/src/Pure/Thy/thy_header.scala Wed Apr 13 18:04:27 2016 +0200
@@ -109,7 +109,7 @@
val args =
position(theory_name) ~
- (opt($$$(IMPORTS) ~! rep1(position(theory_xname))) ^^
+ (opt($$$(IMPORTS) ~! rep1(position(theory_name))) ^^
{ case None => Nil case Some(_ ~ xs) => xs }) ~
(opt($$$(KEYWORDS) ~! keyword_decls) ^^
{ case None => Nil case Some(_ ~ xs) => xs }) ~
--- a/src/Pure/Thy/thy_output.ML Wed Apr 13 14:12:51 2016 +0200
+++ b/src/Pure/Thy/thy_output.ML Wed Apr 13 18:04:27 2016 +0200
@@ -143,7 +143,7 @@
local
val property =
- Parse.position Parse.xname -- Scan.optional (Parse.$$$ "=" |-- Parse.!!! Parse.xname) "";
+ Parse.position Parse.name -- Scan.optional (Parse.$$$ "=" |-- Parse.!!! Parse.name) "";
val properties =
Scan.optional (Parse.$$$ "[" |-- Parse.!!! (Parse.enum "," property --| Parse.$$$ "]")) [];
@@ -404,7 +404,7 @@
val locale =
Scan.option ((Parse.$$$ "(" -- improper -- Parse.$$$ "in") |--
- Parse.!!! (improper |-- Parse.xname --| (improper -- Parse.$$$ ")")));
+ Parse.!!! (improper |-- Parse.name --| (improper -- Parse.$$$ ")")));
in
--- a/src/Pure/Tools/find_consts.ML Wed Apr 13 14:12:51 2016 +0200
+++ b/src/Pure/Tools/find_consts.ML Wed Apr 13 18:04:27 2016 +0200
@@ -136,7 +136,7 @@
local
val criterion =
- Parse.reserved "name" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Name ||
+ Parse.reserved "name" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.name) >> Name ||
Parse.reserved "strict" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.typ) >> Strict ||
Parse.typ >> Loose;
--- a/src/Pure/Tools/find_theorems.ML Wed Apr 13 14:12:51 2016 +0200
+++ b/src/Pure/Tools/find_theorems.ML Wed Apr 13 18:04:27 2016 +0200
@@ -509,7 +509,7 @@
local
val criterion =
- Parse.reserved "name" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Name ||
+ Parse.reserved "name" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.name) >> Name ||
Parse.reserved "intro" >> K Intro ||
Parse.reserved "elim" >> K Elim ||
Parse.reserved "dest" >> K Dest ||
--- a/src/Tools/Code/code_ml.ML Wed Apr 13 14:12:51 2016 +0200
+++ b/src/Tools/Code/code_ml.ML Wed Apr 13 18:04:27 2016 +0200
@@ -871,7 +871,7 @@
check = { env_var = "ISABELLE_TOOL",
make_destination = fn p => Path.append p (Path.explode "ROOT.ML"),
make_command = fn _ =>
- "\"$ISABELLE_TOOL\" process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure" } })
+ "isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure" } })
#> Code_Target.add_language
(target_OCaml, { serializer = serializer_ocaml, literals = literals_ocaml,
check = { env_var = "ISABELLE_OCAML",
--- a/src/Tools/Code/code_target.ML Wed Apr 13 14:12:51 2016 +0200
+++ b/src/Tools/Code/code_target.ML Wed Apr 13 18:04:27 2016 +0200
@@ -104,7 +104,7 @@
fun read_inst ctxt (raw_tyco, raw_class) =
(read_tyco ctxt raw_tyco, Proof_Context.read_class ctxt raw_class);
-val parse_inst_ident = Parse.xname --| @{keyword "::"} -- Parse.class;
+val parse_inst_ident = Parse.name --| @{keyword "::"} -- Parse.class;
fun cert_syms ctxt =
Code_Symbol.map_attr (apfst (cert_const ctxt)) (apfst (cert_tyco ctxt))
--- a/src/ZF/Tools/datatype_package.ML Wed Apr 13 14:12:51 2016 +0200
+++ b/src/ZF/Tools/datatype_package.ML Wed Apr 13 18:04:27 2016 +0200
@@ -433,9 +433,9 @@
("define " ^ coind_prefix ^ "datatype")
((Scan.optional ((@{keyword "\<subseteq>"} || @{keyword "<="}) |-- Parse.!!! Parse.term) "") --
Parse.and_list1 (Parse.term -- (@{keyword "="} |-- Parse.enum1 "|" con_decl)) --
- Scan.optional (@{keyword "monos"} |-- Parse.!!! Parse.xthms1) [] --
- Scan.optional (@{keyword "type_intros"} |-- Parse.!!! Parse.xthms1) [] --
- Scan.optional (@{keyword "type_elims"} |-- Parse.!!! Parse.xthms1) []
+ Scan.optional (@{keyword "monos"} |-- Parse.!!! Parse.thms1) [] --
+ Scan.optional (@{keyword "type_intros"} |-- Parse.!!! Parse.thms1) [] --
+ Scan.optional (@{keyword "type_elims"} |-- Parse.!!! Parse.thms1) []
>> (Toplevel.theory o mk_datatype));
end;
--- a/src/ZF/Tools/induct_tacs.ML Wed Apr 13 14:12:51 2016 +0200
+++ b/src/ZF/Tools/induct_tacs.ML Wed Apr 13 18:04:27 2016 +0200
@@ -192,10 +192,10 @@
val _ =
Outer_Syntax.command @{command_keyword rep_datatype} "represent existing set inductively"
- ((@{keyword "elimination"} |-- Parse.!!! Parse.xthm) --
- (@{keyword "induction"} |-- Parse.!!! Parse.xthm) --
- (@{keyword "case_eqns"} |-- Parse.!!! Parse.xthms1) --
- Scan.optional (@{keyword "recursor_eqns"} |-- Parse.!!! Parse.xthms1) []
+ ((@{keyword "elimination"} |-- Parse.!!! Parse.thm) --
+ (@{keyword "induction"} |-- Parse.!!! Parse.thm) --
+ (@{keyword "case_eqns"} |-- Parse.!!! Parse.thms1) --
+ Scan.optional (@{keyword "recursor_eqns"} |-- Parse.!!! Parse.thms1) []
>> (fn (((x, y), z), w) => Toplevel.theory (rep_datatype x y z w)));
end;
--- a/src/ZF/Tools/inductive_package.ML Wed Apr 13 14:12:51 2016 +0200
+++ b/src/ZF/Tools/inductive_package.ML Wed Apr 13 18:04:27 2016 +0200
@@ -587,10 +587,10 @@
((@{keyword "\<subseteq>"} || @{keyword "<="}) |-- Parse.term))) --
(@{keyword "intros"} |--
Parse.!!! (Scan.repeat1 (Parse_Spec.opt_thm_name ":" -- Parse.prop))) --
- Scan.optional (@{keyword "monos"} |-- Parse.!!! Parse.xthms1) [] --
- Scan.optional (@{keyword "con_defs"} |-- Parse.!!! Parse.xthms1) [] --
- Scan.optional (@{keyword "type_intros"} |-- Parse.!!! Parse.xthms1) [] --
- Scan.optional (@{keyword "type_elims"} |-- Parse.!!! Parse.xthms1) []
+ Scan.optional (@{keyword "monos"} |-- Parse.!!! Parse.thms1) [] --
+ Scan.optional (@{keyword "con_defs"} |-- Parse.!!! Parse.thms1) [] --
+ Scan.optional (@{keyword "type_intros"} |-- Parse.!!! Parse.thms1) [] --
+ Scan.optional (@{keyword "type_elims"} |-- Parse.!!! Parse.thms1) []
>> (Toplevel.theory o mk_ind);
val _ =