# HG changeset patch
# User wenzelm
# Date 1428333610 -7200
# Node ID 6eccb133d4e6f19937868f55b30a15691d0116a4
# Parent  b8ffc3dc9e24fefe2af58f52b7e1e7609970c97a
clarified rail syntax;

diff -r b8ffc3dc9e24 -r 6eccb133d4e6 src/Doc/Isar_Ref/Document_Preparation.thy
--- a/src/Doc/Isar_Ref/Document_Preparation.thy	Mon Apr 06 17:06:48 2015 +0200
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy	Mon Apr 06 17:20:10 2015 +0200
@@ -471,7 +471,7 @@
   \end{matharray}
 
   @{rail \<open>
-    'rail' (@{syntax string} | @{syntax cartouche})
+    'rail' @{syntax text}
   \<close>}
 
   The @{antiquotation rail} antiquotation allows to include syntax
diff -r b8ffc3dc9e24 -r 6eccb133d4e6 src/Pure/Tools/rail.ML
--- a/src/Pure/Tools/rail.ML	Mon Apr 06 17:06:48 2015 +0200
+++ b/src/Pure/Tools/rail.ML	Mon Apr 06 17:20:10 2015 +0200
@@ -363,8 +363,7 @@
 in
 
 val _ = Theory.setup
-  (Thy_Output.antiquotation @{binding rail}
-    (Scan.lift (Parse.input (Parse.string || Parse.cartouche)))
+  (Thy_Output.antiquotation @{binding rail} (Scan.lift Args.text_input)
     (fn {state, context, ...} => output_rules state o read context));
 
 end;