Isar.command: plain Position.id;
tuned;

--- a/src/Pure/Isar/isar.ML	Fri Jan 02 15:44:33 2009 +0100
+++ b/src/Pure/Isar/isar.ML	Fri Jan 02 15:44:59 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/Isar/isar.ML
-    ID:         $Id$
     Author:     Makarius
 
 The global Isabelle/Isar state and main read-eval-print loop.
@@ -377,26 +376,25 @@
 
 local
 
-structure P = OuterParse and K = OuterKeyword;
+structure P = struct open OuterParse open ValueParse end;
 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)))));
+  OuterSyntax.internal_command "Isar.command"
+    (P.string -- P.string >> (fn (id, text) =>
+      Toplevel.imperative (fn () =>
+        ignore (create_command (OuterSyntax.prepare_command (Position.id id) text)))));
 
 val _ =
-  OuterSyntax.improper_command "Isar.insert" "insert command (Isar editor model)" K.control
+  OuterSyntax.internal_command "Isar.insert"
     (P.string -- P.string >> (fn (prev, id) =>
-      Toplevel.no_timing o Toplevel.imperative (fn () => insert_command prev id)));
+      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)));
+  OuterSyntax.internal_command "Isar.remove"
+    (P.string >> (fn id => Toplevel.imperative (fn () => remove_command id)));
 
 end;
 

--- a/src/Pure/Isar/isar.scala	Fri Jan 02 15:44:33 2009 +0100
+++ b/src/Pure/Isar/isar.scala	Fri Jan 02 15:44:59 2009 +0100
@@ -1,22 +1,19 @@
 /*  Title:      Pure/Isar/isar.scala
     Author:     Makarius
 
-Isar toplevel editor model.
+Isar document model.
 */
 
 package isabelle
 
-import java.util.Properties
-
 
 class Isar(isabelle_system: IsabelleSystem, results: EventBus[IsabelleProcess.Result], args: String*)
   extends IsabelleProcess(isabelle_system, results, args: _*)
 {
-
   /* basic editor commands */
 
-  def create_command(props: Properties, text: String) =
-    output_sync("Isar.command " + IsabelleSyntax.encode_properties(props) + " " +
+  def create_command(id: String, text: String) =
+    output_sync("Isar.command " + IsabelleSyntax.encode_string(id) + " " +
       IsabelleSyntax.encode_string(text))
 
   def insert_command(prev: String, id: String) =
@@ -25,5 +22,4 @@
 
   def remove_command(id: String) =
     output_sync("Isar.remove " + IsabelleSyntax.encode_string(id))
-
 }