# HG changeset patch
# User wenzelm
# Date 1221850848 -7200
# Node ID 7804ded330bb9f39bcb561951e4ab7a857a891a5
# Parent  111fc18792504dcb4d4ec1219119bf1c7545dda4
moved Isar editor commands from isar_syn.ML to isar.ML;
P.props_text;

diff -r 111fc1879250 -r 7804ded330bb src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Fri Sep 19 21:00:47 2008 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Fri Sep 19 21:00:48 2008 +0200
@@ -714,13 +714,9 @@
 
 (* nested commands *)
 
-val props_text =
-  Scan.optional P.properties [] -- P.position P.string >> (fn (props, (str, pos)) =>
-    (Position.of_properties (Position.default_properties pos props), str));
-
 val _ =
   OuterSyntax.improper_command "Isabelle.command" "nested Isabelle command" K.control
-    (props_text :|-- (fn (pos, str) =>
+    (P.props_text :|-- (fn (pos, str) =>
       (case OuterSyntax.parse pos str of
         [tr] => Scan.succeed (K tr)
       | _ => Scan.fail_with (K "exactly one command expected"))
@@ -730,22 +726,6 @@
 (* global history commands *)
 
 val _ =
-  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 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 () => 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));