# HG changeset patch
# User wenzelm
# Date 1314988532 -7200
# Node ID 665ebb45bc1aa1ba9870cc34fdc6a8e43d0c23b2
# Parent  5bec9c15ef29e4411e0e110f80c802407218df78
tuned;

diff -r 5bec9c15ef29 -r 665ebb45bc1a src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Fri Sep 02 20:29:39 2011 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Fri Sep 02 20:35:32 2011 +0200
@@ -34,9 +34,9 @@
   val process_file: Path.T -> theory -> theory
   type isar
   val isar: TextIO.instream -> bool -> isar
+  val read_command: Position.T -> string -> Toplevel.transition
   val read_element: outer_syntax -> (unit -> theory) -> Thy_Syntax.element ->
     (Toplevel.transition * Toplevel.transition list) list
-  val read_command: Position.T -> string -> Toplevel.transition
 end;
 
 structure Outer_Syntax: OUTER_SYNTAX =
@@ -270,6 +270,12 @@
     handle ERROR msg => (Toplevel.malformed range_pos msg, true)
   end;
 
+fun read_command pos str =
+  let
+    val (lexs, outer_syntax) = get_syntax ();
+    val toks = Thy_Syntax.parse_tokens lexs pos str;
+  in #1 (read_span outer_syntax toks) end;
+
 fun read_element outer_syntax init {head, proof, proper_proof} =
   let
     val read = read_span outer_syntax o Thy_Syntax.span_content;
@@ -280,11 +286,5 @@
     else map (rpair []) (if proper_head then tr :: proof_trs else proof_trs)
   end;
 
-fun read_command pos str =
-  let
-    val (lexs, outer_syntax) = get_syntax ();
-    val toks = Thy_Syntax.parse_tokens lexs pos str;
-  in #1 (read_span outer_syntax toks) end;
-
 end;