--- a/NEWS Tue May 24 18:48:01 2016 +0200
+++ b/NEWS Tue May 24 19:42:47 2016 +0200
@@ -38,6 +38,9 @@
*** Prover IDE -- Isabelle/Scala/jEdit ***
+* Cartouche abbreviations work both for " and ` to accomodate typical
+situations where old ASCII notation may be updated.
+
* IDE support for the Isabelle/Pure bootstrap process, with the
following independent stages:
--- a/src/Doc/Isar_Ref/Document_Preparation.thy Tue May 24 18:48:01 2016 +0200
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy Tue May 24 19:42:47 2016 +0200
@@ -462,7 +462,7 @@
@{rail \<open>
@{syntax_def tags}: ( tag * )
;
- tag: '%' (@{syntax ident} | @{syntax string})
+ tag: '%' (@{syntax short_ident} | @{syntax string})
\<close>}
Some tags are pre-declared for certain classes of commands, serving as
@@ -538,9 +538,9 @@
\<close>}
\endgroup
- The lexical syntax of \<open>identifier\<close> coincides with that of @{syntax ident} in
- regular Isabelle syntax, but \<open>string\<close> uses single quotes instead of double
- quotes of the standard @{syntax string} category.
+ The lexical syntax of \<open>identifier\<close> coincides with that of @{syntax
+ short_ident} in regular Isabelle syntax, but \<open>string\<close> uses single quotes
+ instead of double quotes of the standard @{syntax string} category.
Each \<open>rule\<close> defines a formal language (with optional name), using a notation
that is similar to EBNF or regular expressions with recursion. The meaning
--- a/src/Doc/Isar_Ref/Inner_Syntax.thy Tue May 24 18:48:01 2016 +0200
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy Tue May 24 19:42:47 2016 +0200
@@ -387,7 +387,7 @@
;
entry: atom ('=' atom)?
;
- atom: @{syntax ident} | @{syntax int} | @{syntax float} | @{syntax cartouche}
+ atom: @{syntax short_ident} | @{syntax int} | @{syntax float} | @{syntax cartouche}
\<close>}
Each @{syntax entry} is a name-value pair: if the value is omitted, if
@@ -556,11 +556,11 @@
\begin{center}
\begin{supertabular}{rcl}
- @{syntax_def (inner) id} & = & @{syntax_ref ident} \\
- @{syntax_def (inner) longid} & = & @{syntax_ref longident} \\
+ @{syntax_def (inner) id} & = & @{syntax_ref short_ident} \\
+ @{syntax_def (inner) longid} & = & @{syntax_ref long_ident} \\
@{syntax_def (inner) var} & = & @{syntax_ref var} \\
- @{syntax_def (inner) tid} & = & @{syntax_ref typefree} \\
- @{syntax_def (inner) tvar} & = & @{syntax_ref typevar} \\
+ @{syntax_def (inner) tid} & = & @{syntax_ref type_ident} \\
+ @{syntax_def (inner) tvar} & = & @{syntax_ref type_var} \\
@{syntax_def (inner) num_token} & = & @{syntax_ref nat} \\
@{syntax_def (inner) float_token} & = & @{syntax_ref nat}\<^verbatim>\<open>.\<close>@{syntax_ref nat} \\
@{syntax_def (inner) str_token} & = & \<^verbatim>\<open>''\<close> \<open>\<dots>\<close> \<^verbatim>\<open>''\<close> \\
--- a/src/Doc/Isar_Ref/Outer_Syntax.thy Tue May 24 18:48:01 2016 +0200
+++ b/src/Doc/Isar_Ref/Outer_Syntax.thy Tue May 24 19:42:47 2016 +0200
@@ -97,14 +97,14 @@
\begin{center}
\begin{supertabular}{rcl}
- @{syntax_def ident} & = & \<open>letter (subscript\<^sup>? quasiletter)\<^sup>*\<close> \\
- @{syntax_def longident} & = & \<open>ident(\<close>\<^verbatim>\<open>.\<close>\<open>ident)\<^sup>+\<close> \\
- @{syntax_def symident} & = & \<open>sym\<^sup>+ |\<close>~~\<^verbatim>\<open>\\<close>\<^verbatim>\<open><\<close>\<open>ident\<close>\<^verbatim>\<open>>\<close> \\
+ @{syntax_def short_ident} & = & \<open>letter (subscript\<^sup>? quasiletter)\<^sup>*\<close> \\
+ @{syntax_def long_ident} & = & \<open>short_ident(\<close>\<^verbatim>\<open>.\<close>\<open>short_ident)\<^sup>+\<close> \\
+ @{syntax_def sym_ident} & = & \<open>sym\<^sup>+ |\<close>~~\<^verbatim>\<open>\\<close>\<^verbatim>\<open><\<close>\<open>short_ident\<close>\<^verbatim>\<open>>\<close> \\
@{syntax_def nat} & = & \<open>digit\<^sup>+\<close> \\
@{syntax_def float} & = & @{syntax_ref nat}\<^verbatim>\<open>.\<close>@{syntax_ref nat}~~\<open>|\<close>~~\<^verbatim>\<open>-\<close>@{syntax_ref nat}\<^verbatim>\<open>.\<close>@{syntax_ref nat} \\
- @{syntax_def var} & = & \<^verbatim>\<open>?\<close>\<open>ident |\<close>~~\<^verbatim>\<open>?\<close>\<open>ident\<close>\<^verbatim>\<open>.\<close>\<open>nat\<close> \\
- @{syntax_def typefree} & = & \<^verbatim>\<open>'\<close>\<open>ident\<close> \\
- @{syntax_def typevar} & = & \<^verbatim>\<open>?\<close>\<open>typefree |\<close>~~\<^verbatim>\<open>?\<close>\<open>typefree\<close>\<^verbatim>\<open>.\<close>\<open>nat\<close> \\
+ @{syntax_def term_var} & = & \<^verbatim>\<open>?\<close>\<open>short_ident |\<close>~~\<^verbatim>\<open>?\<close>\<open>short_ident\<close>\<^verbatim>\<open>.\<close>\<open>nat\<close> \\
+ @{syntax_def type_ident} & = & \<^verbatim>\<open>'\<close>\<open>short_ident\<close> \\
+ @{syntax_def type_var} & = & \<^verbatim>\<open>?\<close>\<open>type_ident |\<close>~~\<^verbatim>\<open>?\<close>\<open>type_ident\<close>\<^verbatim>\<open>.\<close>\<open>nat\<close> \\
@{syntax_def string} & = & \<^verbatim>\<open>"\<close> \<open>\<dots>\<close> \<^verbatim>\<open>"\<close> \\
@{syntax_def altstring} & = & \<^verbatim>\<open>`\<close> \<open>\<dots>\<close> \<^verbatim>\<open>`\<close> \\
@{syntax_def cartouche} & = & @{verbatim "\<open>"} \<open>\<dots>\<close> @{verbatim "\<close>"} \\
@@ -128,13 +128,13 @@
\end{supertabular}
\end{center}
- A @{syntax_ref var} or @{syntax_ref typevar} describes an unknown, which is
- internally a pair of base name and index (ML type @{ML_type indexname}).
- These components are either separated by a dot as in \<open>?x.1\<close> or \<open>?x7.3\<close> or
- run together as in \<open>?x1\<close>. The latter form is possible if the base name does
- not end with digits. If the index is 0, it may be dropped altogether: \<open>?x\<close>
- and \<open>?x0\<close> and \<open>?x.0\<close> all refer to the same unknown, with basename \<open>x\<close> and
- index 0.
+ A @{syntax_ref term_var} or @{syntax_ref type_var} describes an unknown,
+ which is internally a pair of base name and index (ML type @{ML_type
+ indexname}). These components are either separated by a dot as in \<open>?x.1\<close> or
+ \<open>?x7.3\<close> or run together as in \<open>?x1\<close>. The latter form is possible if the base
+ name does not end with digits. If the index is 0, it may be dropped
+ altogether: \<open>?x\<close> and \<open>?x0\<close> and \<open>?x.0\<close> all refer to the same unknown, with
+ basename \<open>x\<close> and index 0.
The syntax of @{syntax_ref string} admits any characters, including
newlines; ``\<^verbatim>\<open>"\<close>'' (double-quote) and ``\<^verbatim>\<open>\\<close>'' (backslash) need to be
@@ -183,8 +183,8 @@
those ruled out by outer syntax keywords (e.g.\ quoted \<^verbatim>\<open>"let"\<close>).
@{rail \<open>
- @{syntax_def name}: @{syntax ident} | @{syntax longident} |
- @{syntax symident} | @{syntax nat} | @{syntax string}
+ @{syntax_def name}: @{syntax short_ident} | @{syntax long_ident} |
+ @{syntax sym_ident} | @{syntax nat} | @{syntax string}
;
@{syntax_def par_name}: '(' @{syntax name} ')'
\<close>}
@@ -221,8 +221,8 @@
@{rail \<open>
@{syntax_def embedded}: @{syntax cartouche} | @{syntax string} |
- @{syntax ident} | @{syntax longident} | @{syntax symident} |
- @{syntax nat}
+ @{syntax short_ident} | @{syntax long_ident} | @{syntax sym_ident} |
+ @{syntax term_var} | @{syntax type_ident} | @{syntax type_var} | @{syntax nat}
\<close>}
\<close>
@@ -238,7 +238,7 @@
Isabelle/Isar commands.
@{rail \<open>
- @{syntax_def text}: @{syntax verbatim} | @{syntax cartouche} | @{syntax name}
+ @{syntax_def text}: @{syntax embedded} | @{syntax verbatim}
;
@{syntax_def comment}: ('--' | @'\<comment>') @{syntax text}
\<close>}
@@ -256,7 +256,7 @@
@{rail \<open>
@{syntax_def classdecl}: @{syntax name} (('<' | '\<subseteq>') (@{syntax name} + ','))?
;
- @{syntax_def sort}: @{syntax name}
+ @{syntax_def sort}: @{syntax embedded}
;
@{syntax_def arity}: ('(' (@{syntax sort} + ',') ')')? @{syntax sort}
\<close>}
@@ -278,12 +278,11 @@
as \<^verbatim>\<open>=\<close> or \<^verbatim>\<open>+\<close>).
@{rail \<open>
- @{syntax_def type}: @{syntax embedded} | @{syntax typefree} |
- @{syntax typevar}
+ @{syntax_def type}: @{syntax embedded}
;
- @{syntax_def term}: @{syntax embedded} | @{syntax var}
+ @{syntax_def term}: @{syntax embedded}
;
- @{syntax_def prop}: @{syntax term}
+ @{syntax_def prop}: @{syntax embedded}
\<close>}
Positional instantiations are specified as a sequence of terms, or the
@@ -305,7 +304,7 @@
;
@{syntax_def named_insts}: (named_inst @'and' +)
;
- variable: @{syntax name} | @{syntax var} | @{syntax typefree} | @{syntax typevar}
+ variable: @{syntax name} | @{syntax term_var} | @{syntax type_ident} | @{syntax type_var}
\<close>}
Type declarations and definitions usually refer to @{syntax typespec} on the
@@ -315,11 +314,11 @@
@{rail \<open>
@{syntax_def typespec}:
- (() | @{syntax typefree} | '(' ( @{syntax typefree} + ',' ) ')') @{syntax name}
+ (() | @{syntax type_ident} | '(' ( @{syntax type_ident} + ',' ) ')') @{syntax name}
;
@{syntax_def typespec_sorts}:
- (() | (@{syntax typefree} ('::' @{syntax sort})?) |
- '(' ( (@{syntax typefree} ('::' @{syntax sort})?) + ',' ) ')') @{syntax name}
+ (() | (@{syntax type_ident} ('::' @{syntax sort})?) |
+ '(' ( (@{syntax type_ident} ('::' @{syntax sort})?) + ',' ) ')') @{syntax name}
\<close>}
\<close>
@@ -387,11 +386,11 @@
The attribute argument specifications may be any sequence of atomic entities
(identifiers, strings etc.), or properly bracketed argument lists. Below
@{syntax atom} refers to any atomic entity, including any @{syntax keyword}
- conforming to @{syntax symident}.
+ conforming to @{syntax sym_ident}.
@{rail \<open>
- @{syntax_def atom}: @{syntax name} | @{syntax typefree} |
- @{syntax typevar} | @{syntax var} | @{syntax nat} | @{syntax float} |
+ @{syntax_def atom}: @{syntax name} | @{syntax type_ident} |
+ @{syntax type_var} | @{syntax term_var} | @{syntax nat} | @{syntax float} |
@{syntax keyword} | @{syntax cartouche}
;
arg: @{syntax atom} | '(' @{syntax args} ')' | '[' @{syntax args} ']'
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Tue May 24 18:48:01 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Tue May 24 19:42:47 2016 +0200
@@ -23,12 +23,13 @@
assumes euclidean_all_zero_iff:
"(\<forall>u\<in>Basis. inner x u = 0) \<longleftrightarrow> (x = 0)"
-abbreviation dimension :: "('a::euclidean_space) itself \<Rightarrow> nat" where
- "dimension TYPE('a) \<equiv> card (Basis :: 'a set)"
-
-syntax "_type_dimension" :: "type => nat" ("(1DIM/(1'(_')))")
-
-translations "DIM('t)" == "CONST dimension (TYPE('t))"
+syntax "_type_dimension" :: "type \<Rightarrow> nat" ("(1DIM/(1'(_')))")
+translations "DIM('a)" \<rightharpoonup> "CONST card (CONST Basis :: 'a set)"
+typed_print_translation \<open>
+ [(@{const_syntax card},
+ fn ctxt => fn _ => fn [Const (@{const_syntax Basis}, Type (@{type_name set}, [T]))] =>
+ Syntax.const @{syntax_const "_type_dimension"} $ Syntax_Phases.term_of_typ ctxt T)]
+\<close>
lemma (in euclidean_space) norm_Basis[simp]: "u \<in> Basis \<Longrightarrow> norm u = 1"
unfolding norm_eq_sqrt_inner by (simp add: inner_Basis)
--- a/src/HOL/Tools/Nitpick/nitpick_commands.ML Tue May 24 18:48:01 2016 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_commands.ML Tue May 24 19:42:47 2016 +0200
@@ -292,7 +292,7 @@
extract_params (Proof_Context.init_global thy) Normal (default_raw_params thy)
o map (apsnd single)
-val parse_key = Scan.repeat1 Parse.typ_group >> space_implode " "
+val parse_key = Scan.repeat1 Parse.embedded >> space_implode " "
val parse_value =
Scan.repeats1 (Parse.minus >> single
|| Scan.repeat1 (Scan.unless Parse.minus
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Tue May 24 18:48:01 2016 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Tue May 24 19:42:47 2016 +0200
@@ -348,7 +348,7 @@
key ^ (case implode_param values of "" => "" | value => " = " ^ value)
val parse_query_bang = @{keyword "?"} || @{keyword "!"} || @{keyword "!!"}
-val parse_key = Scan.repeat1 (Parse.typ_group || parse_query_bang) >> implode_param
+val parse_key = Scan.repeat1 (Parse.embedded || parse_query_bang) >> implode_param
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)) []
--- a/src/Pure/General/completion.scala Tue May 24 18:48:01 2016 +0200
+++ b/src/Pure/General/completion.scala Tue May 24 19:42:47 2016 +0200
@@ -334,7 +334,10 @@
List("@{" -> "@{\u0007}",
"`" -> "\\<close>",
"`" -> "\\<open>",
- "`" -> "\\<open>\u0007\\<close>")
+ "`" -> "\\<open>\u0007\\<close>",
+ "\"" -> "\\<close>",
+ "\"" -> "\\<open>",
+ "\"" -> "\\<open>\u0007\\<close>")
private def default_frequency(name: String): Option[Int] =
default_abbrs.iterator.map(_._2).zipWithIndex.find(_._1 == name).map(_._2)
--- a/src/Pure/Isar/parse.ML Tue May 24 18:48:01 2016 +0200
+++ b/src/Pure/Isar/parse.ML Tue May 24 19:42:47 2016 +0200
@@ -78,7 +78,6 @@
val multi_arity: (string list * string list * string) parser
val type_args: string list parser
val type_args_constrained: (string * string option) list parser
- val typ_group: string parser
val typ: string parser
val mixfix: mixfix parser
val mixfix': mixfix parser
@@ -93,11 +92,9 @@
val for_fixes: (binding * string option * mixfix) list parser
val ML_source: Input.source parser
val document_source: Input.source parser
- val term_group: string parser
- val prop_group: string parser
+ val const: string parser
val term: string parser
val prop: string parser
- val const: string parser
val literal_fact: string parser
val propp: (string * string list) parser
val termp: (string * string list) parser
@@ -268,11 +265,10 @@
val embedded =
group (fn () => "embedded content")
- (short_ident || long_ident || sym_ident || number || string || cartouche);
+ (cartouche || string || short_ident || long_ident || sym_ident ||
+ term_var || type_ident || type_var || number);
-val text =
- group (fn () => "text")
- (short_ident || long_ident || sym_ident || number || string || verbatim || cartouche);
+val text = group (fn () => "text") (embedded || verbatim);
val path = group (fn () => "file name/path specification") name;
@@ -301,12 +297,7 @@
(* types *)
-val typ_group =
- group (fn () => "type")
- (short_ident || long_ident || sym_ident || type_ident || type_var || number ||
- string || cartouche);
-
-val typ = inner_syntax typ_group;
+val typ = group (fn () => "type") (inner_syntax embedded);
fun type_arguments arg =
arg >> single ||
@@ -393,13 +384,9 @@
(* terms *)
-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 = group (fn () => "constant") (inner_syntax embedded);
+val term = group (fn () => "term") (inner_syntax embedded);
+val prop = group (fn () => "proposition") (inner_syntax embedded);
val literal_fact = inner_syntax (group (fn () => "literal fact") (alt_string || cartouche));