tuned;
authorwenzelm
Fri Sep 02 20:35:32 2011 +0200 (2011-09-02 ago)
changeset 44659665ebb45bc1a
parent 44658 5bec9c15ef29
child 44660 90bab3febb6c
tuned;
src/Pure/Isar/outer_syntax.ML
     1.1 --- a/src/Pure/Isar/outer_syntax.ML	Fri Sep 02 20:29:39 2011 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Fri Sep 02 20:35:32 2011 +0200
     1.3 @@ -34,9 +34,9 @@
     1.4    val process_file: Path.T -> theory -> theory
     1.5    type isar
     1.6    val isar: TextIO.instream -> bool -> isar
     1.7 +  val read_command: Position.T -> string -> Toplevel.transition
     1.8    val read_element: outer_syntax -> (unit -> theory) -> Thy_Syntax.element ->
     1.9      (Toplevel.transition * Toplevel.transition list) list
    1.10 -  val read_command: Position.T -> string -> Toplevel.transition
    1.11  end;
    1.12  
    1.13  structure Outer_Syntax: OUTER_SYNTAX =
    1.14 @@ -270,6 +270,12 @@
    1.15      handle ERROR msg => (Toplevel.malformed range_pos msg, true)
    1.16    end;
    1.17  
    1.18 +fun read_command pos str =
    1.19 +  let
    1.20 +    val (lexs, outer_syntax) = get_syntax ();
    1.21 +    val toks = Thy_Syntax.parse_tokens lexs pos str;
    1.22 +  in #1 (read_span outer_syntax toks) end;
    1.23 +
    1.24  fun read_element outer_syntax init {head, proof, proper_proof} =
    1.25    let
    1.26      val read = read_span outer_syntax o Thy_Syntax.span_content;
    1.27 @@ -280,11 +286,5 @@
    1.28      else map (rpair []) (if proper_head then tr :: proof_trs else proof_trs)
    1.29    end;
    1.30  
    1.31 -fun read_command pos str =
    1.32 -  let
    1.33 -    val (lexs, outer_syntax) = get_syntax ();
    1.34 -    val toks = Thy_Syntax.parse_tokens lexs pos str;
    1.35 -  in #1 (read_span outer_syntax toks) end;
    1.36 -
    1.37  end;
    1.38