--- a/NEWS Fri Jan 17 18:12:35 2014 +0100
+++ b/NEWS Fri Jan 17 20:20:20 2014 +0100
@@ -16,6 +16,10 @@
workaround in Isabelle2013-1. The prover process no longer accepts
old identifier syntax with \<^isub> or \<^isup>.
+* Syntax of document antiquotation @{rail} now uses \<newline> instead
+of "\\", to avoid the optical illusion of escaped backslash within
+string token. Minor INCOMPATIBILITY.
+
*** Prover IDE -- Isabelle/Scala/jEdit ***
--- a/src/Doc/Datatypes/Datatypes.thy Fri Jan 17 18:12:35 2014 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy Fri Jan 17 20:20:20 2014 +0100
@@ -458,7 +458,7 @@
\end{matharray}
@{rail "
- @@{command datatype_new} target? @{syntax dt_options}? \\
+ @@{command datatype_new} target? @{syntax dt_options}? \<newline>
(@{syntax dt_name} '=' (@{syntax ctor} + '|') + @'and')
;
@{syntax_def dt_options}: '(' (('no_discs_sels' | 'no_code' | 'rep_compat') + ',') ')'
@@ -511,7 +511,7 @@
mention exactly the same type variables in the same order.
@{rail "
- @{syntax_def ctor}: (name ':')? name (@{syntax ctor_arg} * ) \\
+ @{syntax_def ctor}: (name ':')? name (@{syntax ctor_arg} * ) \<newline>
@{syntax dt_sel_defaults}? mixfix?
"}
@@ -1353,7 +1353,7 @@
\end{matharray}
@{rail "
- @@{command primrec_new} target? fixes \\ @'where' (@{syntax pr_equation} + '|')
+ @@{command primrec_new} target? fixes \<newline> @'where' (@{syntax pr_equation} + '|')
;
@{syntax_def pr_equation}: thmdecl? prop
"}
@@ -1575,7 +1575,7 @@
\end{matharray}
@{rail "
- @@{command codatatype} target? \\
+ @@{command codatatype} target? \<newline>
(@{syntax dt_name} '=' (@{syntax ctor} + '|') + @'and')
"}
@@ -2242,7 +2242,8 @@
\end{matharray}
@{rail "
- (@@{command primcorec} | @@{command primcorecursive}) target? \\ @{syntax pcr_option}? fixes @'where'
+ (@@{command primcorec} | @@{command primcorecursive}) target? \<newline>
+ @{syntax pcr_option}? fixes @'where'
(@{syntax pcr_formula} + '|')
;
@{syntax_def pcr_option}: '(' ('sequential' | 'exhaustive') ')'
@@ -2325,8 +2326,8 @@
\end{matharray}
@{rail "
- @@{command bnf} target? (name ':')? typ \\
- 'map:' term ('sets:' (term +))? 'bd:' term \\
+ @@{command bnf} target? (name ':')? typ \<newline>
+ 'map:' term ('sets:' (term +))? 'bd:' term \<newline>
('wits:' (term +))? ('rel:' term)?
"}
*}
@@ -2416,7 +2417,7 @@
\end{matharray}
@{rail "
- @@{command wrap_free_constructors} target? @{syntax dt_options} \\
+ @@{command wrap_free_constructors} target? @{syntax dt_options} \<newline>
term_list name @{syntax wfc_discs_sels}?
;
@{syntax_def wfc_discs_sels}: name_list (name_list_list name_term_list_list? )?
--- a/src/Doc/IsarImplementation/Logic.thy Fri Jan 17 18:12:35 2014 +0100
+++ b/src/Doc/IsarImplementation/Logic.thy Fri Jan 17 20:20:20 2014 +0100
@@ -791,7 +791,7 @@
;
@@{ML_antiquotation thms} thmrefs
;
- @@{ML_antiquotation lemma} ('(' @'open' ')')? ((prop +) + @'and') \\
+ @@{ML_antiquotation lemma} ('(' @'open' ')')? ((prop +) + @'and') \<newline>
@'by' method method?
"}
--- a/src/Doc/IsarRef/Document_Preparation.thy Fri Jan 17 18:12:35 2014 +0100
+++ b/src/Doc/IsarRef/Document_Preparation.thy Fri Jan 17 20:20:20 2014 +0100
@@ -524,12 +524,10 @@
@{rail "A B C"}
- \item Linebreak @{verbatim "\\\\"} inside
- concatenation\footnote{Strictly speaking, this is only a single
- backslash, but the enclosing @{syntax string} syntax requires a
- second one for escaping.} @{verbatim "A B C \\\\ D E F"}
+ \item Newline inside concatenation
+ @{verbatim "A B C \<newline> D E F"}
- @{rail "A B C \\ D E F"}
+ @{rail "A B C \<newline> D E F"}
\item Variants @{verbatim "A | B | C"}
--- a/src/Doc/IsarRef/Generic.thy Fri Jan 17 18:12:35 2014 +0100
+++ b/src/Doc/IsarRef/Generic.thy Fri Jan 17 20:20:20 2014 +0100
@@ -202,7 +202,7 @@
\end{matharray}
@{rail "
- @@{method subst} ('(' 'asm' ')')? \\ ('(' (@{syntax nat}+) ')')? @{syntax thmref}
+ @@{method subst} ('(' 'asm' ')')? \<newline> ('(' (@{syntax nat}+) ')')? @{syntax thmref}
;
@@{method split} @{syntax thmrefs}
"}
@@ -306,7 +306,7 @@
@{rail "
(@@{method rule_tac} | @@{method erule_tac} | @@{method drule_tac} |
- @@{method frule_tac} | @@{method cut_tac} | @@{method thin_tac}) @{syntax goal_spec}? \\
+ @@{method frule_tac} | @@{method cut_tac} | @@{method thin_tac}) @{syntax goal_spec}? \<newline>
( dynamic_insts @'in' @{syntax thmref} | @{syntax thmrefs} )
;
@@{method subgoal_tac} @{syntax goal_spec}? (@{syntax prop} +)
@@ -925,7 +925,7 @@
@{rail "
@@{command simproc_setup} @{syntax name} '(' (@{syntax term} + '|') ')' '='
- @{syntax text} \\ (@'identifier' (@{syntax nameref}+))?
+ @{syntax text} \<newline> (@'identifier' (@{syntax nameref}+))?
;
@@{attribute simproc} (('add' ':')? | 'del' ':') (@{syntax name}+)
--- a/src/Doc/IsarRef/HOL_Specific.thy Fri Jan 17 18:12:35 2014 +0100
+++ b/src/Doc/IsarRef/HOL_Specific.thy Fri Jan 17 20:20:20 2014 +0100
@@ -99,8 +99,8 @@
@{rail "
(@@{command (HOL) inductive} | @@{command (HOL) inductive_set} |
@@{command (HOL) coinductive} | @@{command (HOL) coinductive_set})
- @{syntax target}? \\
- @{syntax \"fixes\"} (@'for' @{syntax \"fixes\"})? (@'where' clauses)? \\
+ @{syntax target}? \<newline>
+ @{syntax \"fixes\"} (@'for' @{syntax \"fixes\"})? (@'where' clauses)? \<newline>
(@'monos' @{syntax thmrefs})?
;
clauses: (@{syntax thmdecl}? @{syntax prop} + '|')
@@ -268,7 +268,7 @@
@@{command (HOL) primrec} @{syntax target}? @{syntax \"fixes\"} @'where' equations
;
(@@{command (HOL) fun} | @@{command (HOL) function}) @{syntax target}? functionopts?
- @{syntax \"fixes\"} \\ @'where' equations
+ @{syntax \"fixes\"} \<newline> @'where' equations
;
equations: (@{syntax thmdecl}? @{syntax prop} + '|')
@@ -576,7 +576,7 @@
@{rail "
@@{command (HOL) partial_function} @{syntax target}?
- '(' @{syntax nameref} ')' @{syntax \"fixes\"} \\
+ '(' @{syntax nameref} ')' @{syntax \"fixes\"} \<newline>
@'where' @{syntax thmdecl}? @{syntax prop}
"}
@@ -650,7 +650,7 @@
(HOL) "function"} or @{command (HOL) "fun"} should be used instead.
@{rail "
- @@{command (HOL) recdef} ('(' @'permissive' ')')? \\
+ @@{command (HOL) recdef} ('(' @'permissive' ')')? \<newline>
@{syntax name} @{syntax term} (@{syntax prop} +) hints?
;
recdeftc @{syntax thmdecl}? tc
@@ -874,7 +874,7 @@
\end{matharray}
@{rail "
- @@{command (HOL) record} @{syntax typespec_sorts} '=' \\
+ @@{command (HOL) record} @{syntax typespec_sorts} '=' \<newline>
(@{syntax type} '+')? (constdecl +)
;
constdecl: @{syntax name} '::' @{syntax type} @{syntax mixfix}?
@@ -1268,13 +1268,13 @@
@{rail "
@@{command (HOL) quotient_type} (spec);
- spec: @{syntax typespec} @{syntax mixfix}? '=' \\
- @{syntax type} '/' ('partial' ':')? @{syntax term} \\
+ spec: @{syntax typespec} @{syntax mixfix}? '=' \<newline>
+ @{syntax type} '/' ('partial' ':')? @{syntax term} \<newline>
(@'morphisms' @{syntax name} @{syntax name})? (@'parametric' @{syntax thmref})?;
"}
@{rail "
- @@{command (HOL) quotient_definition} constdecl? @{syntax thmdecl}? \\
+ @@{command (HOL) quotient_definition} constdecl? @{syntax thmdecl}? \<newline>
@{syntax term} 'is' @{syntax term};
constdecl: @{syntax name} ('::' @{syntax type})? @{syntax mixfix}?
@@ -1401,7 +1401,7 @@
@{rail "
(@@{command (HOL) specification} | @@{command (HOL) ax_specification})
- '(' (decl +) ')' \\ (@{syntax thmdecl}? @{syntax prop} +)
+ '(' (decl +) ')' \<newline> (@{syntax thmdecl}? @{syntax prop} +)
;
decl: ((@{syntax name} ':')? @{syntax term} '(' @'overloaded' ')'?)
"}
@@ -1627,12 +1627,12 @@
\end{matharray}
@{rail "
- @@{command (HOL) setup_lifting} ('(' 'no_code' ')')? \\
+ @@{command (HOL) setup_lifting} ('(' 'no_code' ')')? \<newline>
@{syntax thmref} @{syntax thmref}? (@'parametric' @{syntax thmref})?;
"}
@{rail "
- @@{command (HOL) lift_definition} @{syntax name} '::' @{syntax type} @{syntax mixfix}? \\
+ @@{command (HOL) lift_definition} @{syntax name} '::' @{syntax type} @{syntax mixfix}? \<newline>
'is' @{syntax term} (@'parametric' @{syntax thmref})?;
"}
@@ -2165,7 +2165,7 @@
@@{command (HOL) nitpick_params}) ( '[' args ']' )?
;
- @@{command (HOL) quickcheck_generator} @{syntax nameref} \\
+ @@{command (HOL) quickcheck_generator} @{syntax nameref} \<newline>
'operations:' ( @{syntax term} +)
;
@@ -2414,8 +2414,8 @@
\end{matharray}
@{rail "
- @@{command (HOL) export_code} ( constexpr + ) \\
- ( ( @'in' target ( @'module_name' @{syntax string} ) ? \\
+ @@{command (HOL) export_code} ( constexpr + ) \<newline>
+ ( ( @'in' target ( @'module_name' @{syntax string} ) ? \<newline>
( @'file' @{syntax string} ) ? ( '(' args ')' ) ?) + ) ?
;
@@ -2480,27 +2480,27 @@
syntax: @{syntax string} | ( @'infix' | @'infixl' | @'infixr' ) @{syntax nat} @{syntax string}
;
- printing_const: symbol_const ( '\<rightharpoonup>' | '=>' ) \\
+ printing_const: symbol_const ( '\<rightharpoonup>' | '=>' ) \<newline>
( '(' target ')' syntax ? + @'and' )
;
- printing_typeconstructor: symbol_typeconstructor ( '\<rightharpoonup>' | '=>' ) \\
+ printing_typeconstructor: symbol_typeconstructor ( '\<rightharpoonup>' | '=>' ) \<newline>
( '(' target ')' syntax ? + @'and' )
;
- printing_class: symbol_class ( '\<rightharpoonup>' | '=>' ) \\
+ printing_class: symbol_class ( '\<rightharpoonup>' | '=>' ) \<newline>
( '(' target ')' @{syntax string} ? + @'and' )
;
- printing_class_relation: symbol_class_relation ( '\<rightharpoonup>' | '=>' ) \\
+ printing_class_relation: symbol_class_relation ( '\<rightharpoonup>' | '=>' ) \<newline>
( '(' target ')' @{syntax string} ? + @'and' )
;
- printing_class_instance: symbol_class_instance ( '\<rightharpoonup>' | '=>' ) \\
+ printing_class_instance: symbol_class_instance ( '\<rightharpoonup>' | '=>' ) \<newline>
( '(' target ')' '-' ? + @'and' )
;
- printing_module: symbol_module ( '\<rightharpoonup>' | '=>' ) \\
+ printing_module: symbol_module ( '\<rightharpoonup>' | '=>' ) \<newline>
( '(' target ')' ( @{syntax string} ( @'attach' ( const + ) ) ? ) ? + @'and' )
;
@@ -2509,19 +2509,19 @@
| printing_module ) + '|' )
;
- @@{command (HOL) code_const} (const + @'and') \\
+ @@{command (HOL) code_const} (const + @'and') \<newline>
( ( '(' target ( syntax ? + @'and' ) ')' ) + )
;
- @@{command (HOL) code_type} (typeconstructor + @'and') \\
+ @@{command (HOL) code_type} (typeconstructor + @'and') \<newline>
( ( '(' target ( syntax ? + @'and' ) ')' ) + )
;
- @@{command (HOL) code_class} (class + @'and') \\
- ( ( '(' target \\ ( @{syntax string} ? + @'and' ) ')' ) + )
+ @@{command (HOL) code_class} (class + @'and') \<newline>
+ ( ( '(' target \<newline> ( @{syntax string} ? + @'and' ) ')' ) + )
;
- @@{command (HOL) code_instance} (( typeconstructor '::' class ) + @'and') \\
+ @@{command (HOL) code_instance} (( typeconstructor '::' class ) + @'and') \<newline>
( ( '(' target ( '-' ? + @'and' ) ')' ) + )
;
@@ -2530,7 +2530,7 @@
@@{command (HOL) code_identifier} ( ( symbol_const | symbol_typeconstructor
| symbol_class | symbol_class_relation | symbol_class_instance
- | symbol_module ) ( '\<rightharpoonup>' | '=>' ) \\
+ | symbol_module ) ( '\<rightharpoonup>' | '=>' ) \<newline>
( '(' target ')' @{syntax string} ? + @'and' ) + '|' )
;
@@ -2540,16 +2540,16 @@
@@{command (HOL) code_monad} const const target
;
- @@{command (HOL) code_reflect} @{syntax string} \\
- ( @'datatypes' ( @{syntax string} '=' ( '_' | ( @{syntax string} + '|' ) + @'and' ) ) ) ? \\
+ @@{command (HOL) code_reflect} @{syntax string} \<newline>
+ ( @'datatypes' ( @{syntax string} '=' ( '_' | ( @{syntax string} + '|' ) + @'and' ) ) ) ? \<newline>
( @'functions' ( @{syntax string} + ) ) ? ( @'file' @{syntax string} ) ?
;
- @@{command (HOL) code_pred} \\( '(' @'modes' ':' modedecl ')')? \\ const
+ @@{command (HOL) code_pred} \<newline> ('(' @'modes' ':' modedecl ')')? \<newline> const
;
- modedecl: (modes | ((const ':' modes) \\
- (@'and' ((const ':' modes @'and') +))?))
+ modedecl: (modes | ((const ':' modes) \<newline>
+ (@'and' ((const ':' modes @'and') +))?))
;
modes: mode @'as' const
--- a/src/Doc/IsarRef/Inner_Syntax.thy Fri Jan 17 18:12:35 2014 +0100
+++ b/src/Doc/IsarRef/Inner_Syntax.thy Fri Jan 17 20:20:20 2014 +0100
@@ -561,9 +561,9 @@
@{rail "
(@@{command type_notation} | @@{command no_type_notation}) @{syntax target}?
- @{syntax mode}? \\ (@{syntax nameref} @{syntax mixfix} + @'and')
+ @{syntax mode}? \<newline> (@{syntax nameref} @{syntax mixfix} + @'and')
;
- (@@{command notation} | @@{command no_notation}) @{syntax target}? @{syntax mode}? \\
+ (@@{command notation} | @@{command no_notation}) @{syntax target}? @{syntax mode}? \<newline>
(@{syntax nameref} @{syntax mixfix} + @'and')
;
@@{command write} @{syntax mode}? (@{syntax nameref} @{syntax mixfix} + @'and')
--- a/src/Doc/IsarRef/Misc.thy Fri Jan 17 18:12:35 2014 +0100
+++ b/src/Doc/IsarRef/Misc.thy Fri Jan 17 20:20:20 2014 +0100
@@ -24,7 +24,7 @@
(@@{command print_theory} | @@{command print_theorems}) ('!'?)
;
- @@{command find_theorems} ('(' @{syntax nat}? 'with_dups'? ')')? \\ (thmcriterion * )
+ @@{command find_theorems} ('(' @{syntax nat}? 'with_dups'? ')')? \<newline> (thmcriterion * )
;
thmcriterion: ('-'?) ('name' ':' @{syntax nameref} | 'intro' | 'elim' | 'dest' |
'solves' | 'simp' ':' @{syntax term} | @{syntax term})
--- a/src/Doc/IsarRef/Proof.thy Fri Jan 17 18:12:35 2014 +0100
+++ b/src/Doc/IsarRef/Proof.thy Fri Jan 17 20:20:20 2014 +0100
@@ -190,7 +190,8 @@
;
@@{command def} (def + @'and')
;
- def: @{syntax thmdecl}? \\ @{syntax name} ('==' | '\<equiv>') @{syntax term} @{syntax term_pat}?
+ def: @{syntax thmdecl}? \<newline>
+ @{syntax name} ('==' | '\<equiv>') @{syntax term} @{syntax term_pat}?
"}
\begin{description}
@@ -1303,10 +1304,11 @@
command.
@{rail "
- @@{method cases} ('(' 'no_simp' ')')? \\
+ @@{method cases} ('(' 'no_simp' ')')? \<newline>
(@{syntax insts} * @'and') rule?
;
- (@@{method induct} | @@{method induction}) ('(' 'no_simp' ')')? (definsts * @'and') \\ arbitrary? taking? rule?
+ (@@{method induct} | @@{method induction})
+ ('(' 'no_simp' ')')? (definsts * @'and') \<newline> arbitrary? taking? rule?
;
@@{method coinduct} @{syntax insts} taking rule?
;
--- a/src/Doc/IsarRef/Spec.thy Fri Jan 17 18:12:35 2014 +0100
+++ b/src/Doc/IsarRef/Spec.thy Fri Jan 17 20:20:20 2014 +0100
@@ -51,7 +51,7 @@
admissible.
@{rail "
- @@{command theory} @{syntax name} imports keywords? \\ @'begin'
+ @@{command theory} @{syntax name} imports keywords? \<newline> @'begin'
;
imports: @'imports' (@{syntax name} +)
;
@@ -211,7 +211,7 @@
locale interpretation (\secref{sec:locale}).
@{rail "
- @@{command bundle} @{syntax target}? \\
+ @@{command bundle} @{syntax target}? \<newline>
@{syntax name} '=' @{syntax thmrefs} (@'for' (@{syntax vars} + @'and'))?
;
(@@{command include} | @@{command including}) (@{syntax nameref}+)
@@ -277,10 +277,10 @@
@{rail "
@@{command axiomatization} @{syntax \"fixes\"}? (@'where' specs)?
;
- @@{command definition} @{syntax target}? \\
+ @@{command definition} @{syntax target}? \<newline>
(decl @'where')? @{syntax thmdecl}? @{syntax prop}
;
- @@{command abbreviation} @{syntax target}? @{syntax mode}? \\
+ @@{command abbreviation} @{syntax target}? @{syntax mode}? \<newline>
(decl @'where')? @{syntax prop}
;
@@ -366,7 +366,7 @@
@{rail "
(@@{command declaration} | @@{command syntax_declaration})
- ('(' @'pervasive' ')')? \\ @{syntax target}? @{syntax text}
+ ('(' @'pervasive' ')')? \<newline> @{syntax target}? @{syntax text}
;
@@{command declare} @{syntax target}? (@{syntax thmrefs} + @'and')
"}
@@ -635,7 +635,7 @@
;
@@{command interpret} @{syntax locale_expr} equations?
;
- @@{command sublocale} (@{syntax nameref} ('<' | '\<subseteq>'))? @{syntax locale_expr} \\
+ @@{command sublocale} (@{syntax nameref} ('<' | '\<subseteq>'))? @{syntax locale_expr} \<newline>
equations?
;
@@{command print_dependencies} '!'? @{syntax locale_expr}
@@ -1260,7 +1260,7 @@
\end{matharray}
@{rail "
- (@@{command lemmas} | @@{command theorems}) @{syntax target}? \\
+ (@@{command lemmas} | @@{command theorems}) @{syntax target}? \<newline>
(@{syntax thmdef}? @{syntax thmrefs} + @'and')
(@'for' (@{syntax vars} + @'and'))?
"}
--- a/src/Doc/ZF/ZF_Isar.thy Fri Jan 17 18:12:35 2014 +0100
+++ b/src/Doc/ZF/ZF_Isar.thy Fri Jan 17 20:20:20 2014 +0100
@@ -67,7 +67,7 @@
;
intros: @'intros' (@{syntax thmdecl}? @{syntax prop} +)
;
- hints: @{syntax (ZF) \"monos\"}? condefs? \\
+ hints: @{syntax (ZF) \"monos\"}? condefs? \<newline>
@{syntax (ZF) typeintros}? @{syntax (ZF) typeelims}?
;
@{syntax_def (ZF) \"monos\"}: @'monos' @{syntax thmrefs}
--- a/src/Pure/Thy/rail.ML Fri Jan 17 18:12:35 2014 +0100
+++ b/src/Pure/Thy/rail.ML Fri Jan 17 20:20:20 2014 +0100
@@ -61,7 +61,8 @@
val scan_space = Scan.many1 (Symbol.is_blank o Symbol_Pos.symbol);
val scan_keyword =
- Scan.one (member (op =) ["|", "*", "+", "?", "(", ")", "\\", ";", ":", "@"] o Symbol_Pos.symbol);
+ Scan.one
+ (member (op =) ["|", "*", "+", "?", "(", ")", "\\<newline>", ";", ":", "@"] o Symbol_Pos.symbol);
val err_prefix = "Rail lexical error: ";
@@ -174,7 +175,7 @@
and body3 x = (body4 :|-- (fn a => $$$ "?" >> K (maybe a) || Scan.succeed a)) x
and body4 x =
($$$ "(" |-- !!! (body0 --| $$$ ")") ||
- $$$ "\\" >> K (Newline 0) ||
+ $$$ "\\<newline>" >> K (Newline 0) ||
ident >> Nonterminal ||
at_mode -- string >> Terminal ||
at_mode -- antiq >> Antiquote) x