more direct Token.range_pos and Outer_Syntax.read_command, bypassing Thy_Syntax.span;
authorwenzelm
Fri Sep 02 20:29:39 2011 +0200 (2011-09-02 ago)
changeset 446585bec9c15ef29
parent 44657 17dbd9d9db38
child 44659 665ebb45bc1a
more direct Token.range_pos and Outer_Syntax.read_command, bypassing Thy_Syntax.span;
src/Pure/Isar/outer_syntax.ML
src/Pure/Isar/token.ML
src/Pure/Thy/thy_syntax.ML
     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  
     2.1 --- a/src/Pure/Isar/token.ML	Fri Sep 02 19:25:44 2011 +0200
     2.2 +++ b/src/Pure/Isar/token.ML	Fri Sep 02 20:29:39 2011 +0200
     2.3 @@ -18,6 +18,7 @@
     2.4    val position_of: T -> Position.T
     2.5    val end_position_of: T -> Position.T
     2.6    val pos_of: T -> string
     2.7 +  val range: T list -> Position.range
     2.8    val eof: T
     2.9    val is_eof: T -> bool
    2.10    val not_eof: T -> bool
    2.11 @@ -122,6 +123,13 @@
    2.12  
    2.13  val pos_of = Position.str_of o position_of;
    2.14  
    2.15 +fun range [] = (Position.none, Position.none)
    2.16 +  | range toks =
    2.17 +      let
    2.18 +        val start_pos = position_of (hd toks);
    2.19 +        val end_pos = end_position_of (List.last toks);
    2.20 +      in (start_pos, end_pos) end;
    2.21 +
    2.22  
    2.23  (* control tokens *)
    2.24  
     3.1 --- a/src/Pure/Thy/thy_syntax.ML	Fri Sep 02 19:25:44 2011 +0200
     3.2 +++ b/src/Pure/Thy/thy_syntax.ML	Fri Sep 02 20:29:39 2011 +0200
     3.3 @@ -16,7 +16,6 @@
     3.4    type span
     3.5    val span_kind: span -> span_kind
     3.6    val span_content: span -> Token.T list
     3.7 -  val span_range: span -> Position.range
     3.8    val span_source: (Token.T, 'a) Source.source -> (span, (Token.T, 'a) Source.source) Source.source
     3.9    val parse_spans: Scan.lexicon * Scan.lexicon -> Position.T -> string -> span list
    3.10    val present_span: span -> Output.output
    3.11 @@ -101,15 +100,6 @@
    3.12  fun span_kind (Span (k, _)) = k;
    3.13  fun span_content (Span (_, toks)) = toks;
    3.14  
    3.15 -fun span_range span =
    3.16 -  (case span_content span of
    3.17 -    [] => (Position.none, Position.none)
    3.18 -  | toks =>
    3.19 -      let
    3.20 -        val start_pos = Token.position_of (hd toks);
    3.21 -        val end_pos = Token.end_position_of (List.last toks);
    3.22 -      in (start_pos, end_pos) end);
    3.23 -
    3.24  
    3.25  (* parse *)
    3.26