src/Pure/Isar/outer_syntax.ML

   val local_theory_to_proof: string -> string -> OuterKeyword.T ->
     (OuterParse.token list -> (local_theory -> Proof.state) * OuterLex.token list) -> unit
   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
   val load_thy: Path.T -> string -> Position.T -> string list -> bool -> unit
 end;

   |> Symbol.source false
   |> T.source (SOME false) OuterKeyword.get_lexicons pos
   |> 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 *)
 
 fun process_file path thy =
   let