# HG changeset patch
# User wenzelm
# Date 1216154278 -7200
# Node ID f38c25d106a7d36ddb0bf080517eebdc3420814a
# Parent  0e03b957c6494218d1390ed6572b5030ccacf3b3
renamed IsarCmd.nested_command to OuterSyntax.prepare_command;

diff -r 0e03b957c649 -r f38c25d106a7 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Tue Jul 15 22:37:55 2008 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Tue Jul 15 22:37:58 2008 +0200
@@ -46,7 +46,6 @@
   val disable_pr: Toplevel.transition -> Toplevel.transition
   val enable_pr: Toplevel.transition -> Toplevel.transition
   val ml_diag: bool -> string * Position.T -> Toplevel.transition -> Toplevel.transition
-  val nested_command: Markup.property list -> string * Position.T -> Toplevel.transition
   val cd: Path.T -> Toplevel.transition -> Toplevel.transition
   val pwd: Toplevel.transition -> Toplevel.transition
   val display_drafts: Path.T list -> Toplevel.transition -> Toplevel.transition
@@ -331,16 +330,6 @@
   (ML_Context.eval_in (try Toplevel.generic_theory_of state) verbose pos txt));
 
 
-(* nested commands *)
-
-fun nested_command props (str, pos) =
-  let val pos' = Position.of_properties (props |> Position.default_properties pos) in
-    (case OuterSyntax.parse pos' str of
-      [transition] => transition
-    | _ => error "exactly one command expected")
-  end;
-
-
 (* current working directory *)
 
 fun cd path = Toplevel.imperative (fn () => (File.cd path));
diff -r 0e03b957c649 -r f38c25d106a7 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Tue Jul 15 22:37:55 2008 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Tue Jul 15 22:37:58 2008 +0200
@@ -705,12 +705,12 @@
     (Scan.succeed (Toplevel.print o Toplevel.actual_proof ProofNode.back o Toplevel.skip_proof I));
 
 
-(* nested command *)
+(* nested commands *)
 
 val _ =
   OuterSyntax.improper_command "Isabelle.command" "nested Isabelle command" K.control
-    ((Scan.optional P.properties [] -- P.position P.string) :|-- (fn (props, arg) =>
-      Scan.succeed (K (IsarCmd.nested_command props arg))
+    ((Scan.optional P.properties [] -- P.position P.string) :|-- (fn (props, text) =>
+      Scan.succeed (K (OuterSyntax.prepare_command props text))
         handle ERROR msg => Scan.fail_with (K msg)));
 
 
@@ -993,3 +993,4 @@
     (Scan.succeed (Toplevel.no_timing o IsarCmd.welcome));
 
 end;
+
diff -r 0e03b957c649 -r f38c25d106a7 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Tue Jul 15 22:37:55 2008 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Tue Jul 15 22:37:58 2008 +0200
@@ -24,6 +24,7 @@
   val print_outer_syntax: unit -> unit
   val scan: string -> OuterLex.token list
   val parse: Position.T -> string -> Toplevel.transition list
+  val prepare_command: Markup.property list -> string * Position.T -> Toplevel.transition
   val process_file: Path.T -> theory -> theory
   type isar
   val isar: bool -> isar
@@ -195,6 +196,13 @@
   |> toplevel_source false NONE get_parser
   |> Source.exhaust;
 
+fun prepare_command props (str, pos) =
+  let val pos' = Position.of_properties (props |> Position.default_properties pos) in
+    (case parse pos' str of
+      [transition] => transition
+    | _ => error "exactly one command expected")
+  end;
+
 
 (* process file *)