src/Pure/Isar/isar_syn.ML

 
 
 (* 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));
 
 val _ =
   OuterSyntax.improper_command "linear_undo" "undo commands" K.control