src/Pure/Isar/isar_syn.ML
changeset 26396 e44c5a1a47bd
parent 26385 ae7564661e76
child 26404 56fd70fb7571
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Tue Mar 25 21:01:01 2008 +0100
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Tue Mar 25 21:01:02 2008 +0100
     1.3 @@ -310,7 +310,11 @@
     1.4      (P.position P.text >> IsarCmd.use_mltext true);
     1.5  
     1.6  val _ =
     1.7 -  OuterSyntax.command "ML_command" "eval ML text" (K.tag_ml K.diag)
     1.8 +  OuterSyntax.command "ML_val" "eval ML text (diagnostic)" (K.tag_ml K.diag)
     1.9 +    (P.position P.text >> IsarCmd.use_mltext true);
    1.10 +
    1.11 +val _ =
    1.12 +  OuterSyntax.command "ML_command" "silently eval ML text (diagnostic)" (K.tag_ml K.diag)
    1.13      (P.position P.text >> (Toplevel.no_timing oo IsarCmd.use_mltext false));
    1.14  
    1.15  val _ =