# 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 \ - 'rail' (@{syntax string} | @{syntax cartouche}) + 'rail' @{syntax text} \} 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;