# HG changeset patch
# User wenzelm
# Date 1221850847 -7200
# Node ID 111fc18792504dcb4d4ec1219119bf1c7545dda4
# Parent  14ab7a17e92bb2a725d9a27dd552157c732d1b55
moved Isar editor commands from isar_syn.ML to isar.ML;

diff -r 14ab7a17e92b -r 111fc1879250 src/Pure/Isar/isar.ML
--- a/src/Pure/Isar/isar.ML	Fri Sep 19 21:00:46 2008 +0200
+++ b/src/Pure/Isar/isar.ML	Fri Sep 19 21:00:47 2008 +0200
@@ -233,7 +233,7 @@
 
 (* interactive state transformations *)
 
-nonfix >> >>>;
+local nonfix >> >>> in
 
 fun >> raw_tr =
   let
@@ -257,6 +257,8 @@
 fun >>> [] = ()
   | >>> (tr :: trs) = if >> tr then >>> trs else ();
 
+end;
+
 
 (* implicit navigation wrt. proper commands *)
 
@@ -350,7 +352,7 @@
       (case run true (#transition (the_command id)) state of
         NONE => ()
       | SOME status => report_update_status status id));
-      
+
 fun rerun_commands ids =
   (List.app (report_update_status Unprocessed) ids; List.app try_run ids);
 
@@ -374,5 +376,32 @@
       fold (fn next => add_edge (prev, next)) nexts);
   in descendant_commands nexts end) |> rerun_commands;
 
+
+(* concrete syntax *)
+
+local
+
+structure P = OuterParse and K = OuterKeyword;
+val op >> = Scan.>>;
+
+in
+
+val _ =
+  OuterSyntax.improper_command "Isar.command" "define command (Isar editor model)" K.control
+    (P.props_text >> (fn (pos, str) =>
+      Toplevel.no_timing o Toplevel.imperative (fn () =>
+        ignore (create_command (OuterSyntax.prepare_command pos str)))));
+
+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 () => 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 () => remove_command id)));
+
 end;
 
+end;