# HG changeset patch
# User wenzelm
# Date 1216200025 -7200
# Node ID dee36037a8329123a44a6a59a14484e093b9f18b
# Parent  a811269b577ccd9e2814083783bc9e506b29b0cf
added Isar.command, Isar.insert, Isar.remove (editor model);

diff -r a811269b577c -r dee36037a832 src/Pure/Isar/isar_syn.ML
--- 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));