added Isar.command, Isar.insert, Isar.remove (editor model);

--- a/src/Pure/Isar/isar_syn.ML	Wed Jul 16 11:20:24 2008 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Wed Jul 16 11:20:25 2008 +0200
@@ -717,6 +717,22 @@
 (* global history commands *)
 
 val _ =
+  OuterSyntax.improper_command "Isar.command" "define command (Isar editor model)" K.control
+    (Scan.optional P.properties [] -- P.position P.string >> (fn (props, text) =>
+      Toplevel.no_timing o Toplevel.imperative (fn () =>
+        ignore (Isar.create_command (OuterSyntax.prepare_command props text)))));
+
+val _ =
+  OuterSyntax.improper_command "Isar.insert" "insert command (Isar editor model)" K.control
+    (P.string -- P.string >> (fn (prev, id) =>
+      Toplevel.no_timing o Toplevel.imperative (fn () => Isar.insert_command prev id)));
+
+val _ =
+  OuterSyntax.improper_command "Isar.remove" "remove command (Isar editor model)" K.control
+    (P.string >> (fn id =>
+      Toplevel.no_timing o Toplevel.imperative (fn () => Isar.remove_command id)));
+
+val _ =
   OuterSyntax.improper_command "init_toplevel" "init toplevel point-of-interest" K.control
     (Scan.succeed (Toplevel.no_timing o Toplevel.imperative Isar.init_point));