tuned signature -- prefer quasi-abstract Symbol_Pos.source;
authorwenzelm
Wed Aug 27 12:32:42 2014 +0200 (2014-08-27)
changeset 580479f3826352b52
parent 58046 2873ca3f4b33
child 58048 aa6296d09e0e
tuned signature -- prefer quasi-abstract Symbol_Pos.source;
src/Pure/General/symbol_pos.ML
src/Pure/Isar/attrib.ML
src/Pure/Syntax/syntax.ML
src/Pure/Syntax/syntax_phases.ML
     1.1 --- a/src/Pure/General/symbol_pos.ML	Wed Aug 27 12:32:07 2014 +0200
     1.2 +++ b/src/Pure/General/symbol_pos.ML	Wed Aug 27 12:32:42 2014 +0200
     1.3 @@ -41,6 +41,7 @@
     1.4    val implode_range: Position.T -> Position.T -> T list -> text * Position.range
     1.5    val explode: text * Position.T -> T list
     1.6    type source = {delimited: bool, text: text, pos: Position.T}
     1.7 +  val source_explode: source -> T list
     1.8    val source_content: source -> string * Position.T
     1.9    val scan_ident: T list -> T list * T list
    1.10    val is_identifier: string -> bool
    1.11 @@ -261,6 +262,8 @@
    1.12  
    1.13  type source = {delimited: bool, text: text, pos: Position.T};
    1.14  
    1.15 +fun source_explode {delimited = _, text, pos} = explode (text, pos);
    1.16 +
    1.17  fun source_content {delimited = _, text, pos} =
    1.18    let val syms = explode (text, pos) in (content syms, pos) end;
    1.19  
     2.1 --- a/src/Pure/Isar/attrib.ML	Wed Aug 27 12:32:07 2014 +0200
     2.2 +++ b/src/Pure/Isar/attrib.ML	Wed Aug 27 12:32:42 2014 +0200
     2.3 @@ -49,7 +49,7 @@
     2.4    val thms: thm list context_parser
     2.5    val multi_thm: thm list context_parser
     2.6    val check_attribs: Proof.context -> Token.src list -> Token.src list
     2.7 -  val read_attribs: Proof.context -> Symbol_Pos.text * Position.T -> Token.src list
     2.8 +  val read_attribs: Proof.context -> Symbol_Pos.source -> Token.src list
     2.9    val transform_facts: morphism ->
    2.10      (Attrib.binding * (thm list * Token.src list) list) list ->
    2.11      (Attrib.binding * (thm list * Token.src list) list) list
    2.12 @@ -286,14 +286,14 @@
    2.13      val _ = map (attribute ctxt) srcs;
    2.14    in srcs end;
    2.15  
    2.16 -fun read_attribs ctxt (text, pos) =
    2.17 +fun read_attribs ctxt source =
    2.18    let
    2.19 +    val syms = Symbol_Pos.source_explode source;
    2.20      val lex = #1 (Keyword.get_lexicons ());
    2.21 -    val syms = Symbol_Pos.explode (text, pos);
    2.22    in
    2.23 -    (case Token.read lex Parse.attribs (syms, pos) of
    2.24 +    (case Token.read lex Parse.attribs (syms, #pos source) of
    2.25        [raw_srcs] => check_attribs ctxt raw_srcs
    2.26 -    | _ => error ("Malformed attributes" ^ Position.here pos))
    2.27 +    | _ => error ("Malformed attributes" ^ Position.here (#pos source)))
    2.28    end;
    2.29  
    2.30  
     3.1 --- a/src/Pure/Syntax/syntax.ML	Wed Aug 27 12:32:07 2014 +0200
     3.2 +++ b/src/Pure/Syntax/syntax.ML	Wed Aug 27 12:32:42 2014 +0200
     3.3 @@ -185,10 +185,10 @@
     3.4    let
     3.5      fun parse_tree tree =
     3.6        let
     3.7 -        val {delimited, text, pos} = token_source tree;
     3.8 -        val syms = Symbol_Pos.explode (text, pos);
     3.9 -        val _ = Context_Position.report ctxt pos (markup delimited);
    3.10 -      in parse (syms, pos) end;
    3.11 +        val source = token_source tree;
    3.12 +        val syms = Symbol_Pos.source_explode source;
    3.13 +        val _ = Context_Position.report ctxt (#pos source) (markup (#delimited source));
    3.14 +      in parse (syms, #pos source) end;
    3.15    in
    3.16      (case YXML.parse_body str handle Fail msg => error msg of
    3.17        body as [tree as XML.Elem ((name, _), _)] =>
     4.1 --- a/src/Pure/Syntax/syntax_phases.ML	Wed Aug 27 12:32:07 2014 +0200
     4.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Wed Aug 27 12:32:42 2014 +0200
     4.3 @@ -461,11 +461,11 @@
     4.4            else decode_appl ps asts
     4.5        | decode ps (Ast.Appl asts) = decode_appl ps asts;
     4.6  
     4.7 -    val {text, pos, ...} = Syntax.read_token str;
     4.8 -    val syms = Symbol_Pos.explode (text, pos);
     4.9 +    val source = Syntax.read_token str;
    4.10 +    val syms = Symbol_Pos.source_explode source;
    4.11      val ast =
    4.12 -      parse_asts ctxt true root (syms, pos)
    4.13 -      |> uncurry (report_result ctxt pos)
    4.14 +      parse_asts ctxt true root (syms, #pos source)
    4.15 +      |> uncurry (report_result ctxt (#pos source))
    4.16        |> decode [];
    4.17      val _ = Context_Position.reports_text ctxt (! reports);
    4.18    in ast end;