clarified rail syntax;
authorwenzelm
Mon Apr 06 17:20:10 2015 +0200 (2015-04-06)
changeset 599376eccb133d4e6
parent 59936 b8ffc3dc9e24
child 59938 f84b93187ab6
clarified rail syntax;
src/Doc/Isar_Ref/Document_Preparation.thy
src/Pure/Tools/rail.ML
     1.1 --- a/src/Doc/Isar_Ref/Document_Preparation.thy	Mon Apr 06 17:06:48 2015 +0200
     1.2 +++ b/src/Doc/Isar_Ref/Document_Preparation.thy	Mon Apr 06 17:20:10 2015 +0200
     1.3 @@ -471,7 +471,7 @@
     1.4    \end{matharray}
     1.5  
     1.6    @{rail \<open>
     1.7 -    'rail' (@{syntax string} | @{syntax cartouche})
     1.8 +    'rail' @{syntax text}
     1.9    \<close>}
    1.10  
    1.11    The @{antiquotation rail} antiquotation allows to include syntax
     2.1 --- a/src/Pure/Tools/rail.ML	Mon Apr 06 17:06:48 2015 +0200
     2.2 +++ b/src/Pure/Tools/rail.ML	Mon Apr 06 17:20:10 2015 +0200
     2.3 @@ -363,8 +363,7 @@
     2.4  in
     2.5  
     2.6  val _ = Theory.setup
     2.7 -  (Thy_Output.antiquotation @{binding rail}
     2.8 -    (Scan.lift (Parse.input (Parse.string || Parse.cartouche)))
     2.9 +  (Thy_Output.antiquotation @{binding rail} (Scan.lift Args.text_input)
    2.10      (fn {state, context, ...} => output_rules state o read context));
    2.11  
    2.12  end;