src/Pure/Isar/outer_syntax.ML
changeset 44658 5bec9c15ef29
parent 44478 4fdb1009a370
child 44659 665ebb45bc1a
     1.1 --- a/src/Pure/Isar/outer_syntax.ML	Fri Sep 02 19:25:44 2011 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Fri Sep 02 20:29:39 2011 +0200
     1.3 @@ -34,7 +34,6 @@
     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_span: outer_syntax -> Thy_Syntax.span -> Toplevel.transition * bool
     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 @@ -255,17 +254,16 @@
    1.12  
    1.13  val not_singleton = "Exactly one command expected";
    1.14  
    1.15 -fun read_span outer_syntax span =
    1.16 +fun read_span outer_syntax toks =
    1.17    let
    1.18      val commands = lookup_commands outer_syntax;
    1.19 -    val range_pos = Position.set_range (Thy_Syntax.span_range span);
    1.20 -    val toks = Thy_Syntax.span_content span;
    1.21 +    val range_pos = Position.set_range (Token.range toks);
    1.22      val _ = List.app Thy_Syntax.report_token toks;
    1.23    in
    1.24      (case Source.exhaust (toplevel_source false NONE (K commands) (Source.of_list toks)) of
    1.25        [tr] =>
    1.26          if Keyword.is_control (Toplevel.name_of tr) then
    1.27 -          (Toplevel.malformed range_pos "Illegal control command", true)
    1.28 +          (Toplevel.malformed (Toplevel.pos_of tr) "Illegal control command", true)
    1.29          else (tr, true)
    1.30      | [] => (Toplevel.ignored range_pos, false)
    1.31      | _ => (Toplevel.malformed range_pos not_singleton, true))
    1.32 @@ -274,19 +272,19 @@
    1.33  
    1.34  fun read_element outer_syntax init {head, proof, proper_proof} =
    1.35    let
    1.36 -    val (tr, proper_head) = read_span outer_syntax head |>> Toplevel.modify_init init;
    1.37 -    val proof_trs = map (read_span outer_syntax) proof |> filter #2 |> map #1;
    1.38 +    val read = read_span outer_syntax o Thy_Syntax.span_content;
    1.39 +    val (tr, proper_head) = read head |>> Toplevel.modify_init init;
    1.40 +    val proof_trs = map read proof |> filter #2 |> map #1;
    1.41    in
    1.42      if proper_head andalso proper_proof then [(tr, proof_trs)]
    1.43      else map (rpair []) (if proper_head then tr :: proof_trs else proof_trs)
    1.44    end;
    1.45  
    1.46  fun read_command pos str =
    1.47 -  let val (lexs, outer_syntax) = get_syntax () in
    1.48 -    (case Thy_Syntax.parse_spans lexs pos str of
    1.49 -      [span] => #1 (read_span outer_syntax span)
    1.50 -    | _ => Toplevel.malformed pos not_singleton)
    1.51 -  end;
    1.52 +  let
    1.53 +    val (lexs, outer_syntax) = get_syntax ();
    1.54 +    val toks = Thy_Syntax.parse_tokens lexs pos str;
    1.55 +  in #1 (read_span outer_syntax toks) end;
    1.56  
    1.57  end;
    1.58