Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
added props_text (from outer_parse.ML);
authorwenzelm
Fri, 02 Jan 2009 15:44:32 +0100
changeset 29309 aa6d11fbe3b6
parent 29308 ddf7fad4448c
child 29310 1a633304fa5e
added props_text (from outer_parse.ML);
src/Pure/Isar/isar_syn.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/isar_syn.ML	Fri Jan 02 15:44:32 2009 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Fri Jan 02 15:44:32 2009 +0100
@@ -757,9 +757,13 @@
 
 (* nested commands *)
 
+val props_text =
+  Scan.optional ValueParse.properties [] -- P.position P.string >> (fn (props, (str, pos)) =>
+    (Position.of_properties (Position.default_properties pos props), str));
+
 val _ =
   OuterSyntax.improper_command "Isabelle.command" "nested Isabelle command" K.control
-    (P.props_text :|-- (fn (pos, str) =>
+    (props_text :|-- (fn (pos, str) =>
       (case OuterSyntax.parse pos str of
         [tr] => Scan.succeed (K tr)
       | _ => Scan.fail_with (K "exactly one command expected"))
isabelle