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 'ML_val' command (diagnostic);
authorwenzelm
Tue, 25 Mar 2008 21:01:02 +0100
changeset 26396 e44c5a1a47bd
parent 26395 9e0e4ce51313
child 26397 df68e8dfd0e3
added 'ML_val' command (diagnostic);
src/Pure/Isar/isar_syn.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/isar_syn.ML	Tue Mar 25 21:01:01 2008 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Tue Mar 25 21:01:02 2008 +0100
@@ -310,7 +310,11 @@
     (P.position P.text >> IsarCmd.use_mltext true);
 
 val _ =
-  OuterSyntax.command "ML_command" "eval ML text" (K.tag_ml K.diag)
+  OuterSyntax.command "ML_val" "eval ML text (diagnostic)" (K.tag_ml K.diag)
+    (P.position P.text >> IsarCmd.use_mltext true);
+
+val _ =
+  OuterSyntax.command "ML_command" "silently eval ML text (diagnostic)" (K.tag_ml K.diag)
     (P.position P.text >> (Toplevel.no_timing oo IsarCmd.use_mltext false));
 
 val _ =
isabelle