src/Pure/Isar/isar_syn.ML
changeset 26396 e44c5a1a47bd
parent 26385 ae7564661e76
child 26404 56fd70fb7571
equal deleted inserted replaced
26395:9e0e4ce51313 26396:e44c5a1a47bd
   308 val _ =
   308 val _ =
   309   OuterSyntax.command "ML" "eval ML text (diagnostic)" (K.tag_ml K.diag)
   309   OuterSyntax.command "ML" "eval ML text (diagnostic)" (K.tag_ml K.diag)
   310     (P.position P.text >> IsarCmd.use_mltext true);
   310     (P.position P.text >> IsarCmd.use_mltext true);
   311 
   311 
   312 val _ =
   312 val _ =
   313   OuterSyntax.command "ML_command" "eval ML text" (K.tag_ml K.diag)
   313   OuterSyntax.command "ML_val" "eval ML text (diagnostic)" (K.tag_ml K.diag)
       
   314     (P.position P.text >> IsarCmd.use_mltext true);
       
   315 
       
   316 val _ =
       
   317   OuterSyntax.command "ML_command" "silently eval ML text (diagnostic)" (K.tag_ml K.diag)
   314     (P.position P.text >> (Toplevel.no_timing oo IsarCmd.use_mltext false));
   318     (P.position P.text >> (Toplevel.no_timing oo IsarCmd.use_mltext false));
   315 
   319 
   316 val _ =
   320 val _ =
   317   OuterSyntax.command "ML_setup" "eval ML text (may change theory)" (K.tag_ml K.thy_decl)
   321   OuterSyntax.command "ML_setup" "eval ML text (may change theory)" (K.tag_ml K.thy_decl)
   318     (P.position P.text >> IsarCmd.use_mltext_theory);
   322     (P.position P.text >> IsarCmd.use_mltext_theory);