# HG changeset patch
# User wenzelm
# Date 1218569275 -7200
# Node ID 0340fd7cccc3b225cd0644646bdbcb52ca674eee
# Parent  dc073b565c56ad9bd4da2150fa900594e56ee465
Isabelle.command: inline former OuterSyntax.prepare_command;
Isar.command: based on fail-safe OuterSyntax.prepare_command;

diff -r dc073b565c56 -r 0340fd7cccc3 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Tue Aug 12 21:27:53 2008 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Tue Aug 12 21:27:55 2008 +0200
@@ -713,8 +713,10 @@
 val _ =
   OuterSyntax.improper_command "Isabelle.command" "nested Isabelle command" K.control
     (props_text :|-- (fn (pos, str) =>
-      Scan.succeed (K (OuterSyntax.prepare_command pos str))
-        handle ERROR msg => Scan.fail_with (K msg)));
+      (case OuterSyntax.parse pos str of
+        [tr] => Scan.succeed (K tr)
+      | _ => Scan.fail_with (K "exactly one command expected"))
+      handle ERROR msg => Scan.fail_with (K msg)));
 
 
 (* global history commands *)
@@ -723,7 +725,7 @@
   OuterSyntax.improper_command "Isar.command" "define command (Isar editor model)" K.control
     (props_text >> (fn (pos, str) =>
       Toplevel.no_timing o Toplevel.imperative (fn () =>
-        ignore (Isar.create_command (OuterSyntax.prepare_command_failsafe pos str)))));
+        ignore (Isar.create_command (OuterSyntax.prepare_command pos str)))));
 
 val _ =
   OuterSyntax.improper_command "Isar.insert" "insert command (Isar editor model)" K.control