# HG changeset patch
# User wenzelm
# Date 1389986420 -3600
# Node ID 61a6bf7d4b02402df6008a62c63105fcb4111c2c
# Parent  00e849f5b397e9b5c56dc7018af50be7739fac4b
clarified @{rail} syntax: prefer explicit \<newline> symbol;

diff -r 00e849f5b397 -r 61a6bf7d4b02 NEWS
--- 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 ***
 
diff -r 00e849f5b397 -r 61a6bf7d4b02 src/Doc/Datatypes/Datatypes.thy
--- 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? )?
diff -r 00e849f5b397 -r 61a6bf7d4b02 src/Doc/IsarImplementation/Logic.thy
--- 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?
   "}
 
diff -r 00e849f5b397 -r 61a6bf7d4b02 src/Doc/IsarRef/Document_Preparation.thy
--- 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"}
 
diff -r 00e849f5b397 -r 61a6bf7d4b02 src/Doc/IsarRef/Generic.thy
--- 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}+)
diff -r 00e849f5b397 -r 61a6bf7d4b02 src/Doc/IsarRef/HOL_Specific.thy
--- 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
diff -r 00e849f5b397 -r 61a6bf7d4b02 src/Doc/IsarRef/Inner_Syntax.thy
--- 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')
diff -r 00e849f5b397 -r 61a6bf7d4b02 src/Doc/IsarRef/Misc.thy
--- 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})
diff -r 00e849f5b397 -r 61a6bf7d4b02 src/Doc/IsarRef/Proof.thy
--- 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?
     ;
diff -r 00e849f5b397 -r 61a6bf7d4b02 src/Doc/IsarRef/Spec.thy
--- 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'))?
   "}
diff -r 00e849f5b397 -r 61a6bf7d4b02 src/Doc/ZF/ZF_Isar.thy
--- 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}
diff -r 00e849f5b397 -r 61a6bf7d4b02 src/Pure/Thy/rail.ML
--- 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