more operations;
authorwenzelm
Wed Mar 30 14:52:23 2016 +0200 (2016-03-30)
changeset 62759d16b2ec535ba
parent 62758 c439a7348138
child 62760 aabcc727aa2d
more operations;
src/Pure/General/input.ML
src/Pure/Syntax/mixfix.ML
     1.1 --- a/src/Pure/General/input.ML	Wed Mar 30 14:35:41 2016 +0200
     1.2 +++ b/src/Pure/General/input.ML	Wed Mar 30 14:52:23 2016 +0200
     1.3 @@ -13,6 +13,7 @@
     1.4    val range_of: source -> Position.range
     1.5    val source: bool -> Symbol_Pos.text -> Position.range -> source
     1.6    val string: string -> source
     1.7 +  val reset_pos: source -> source
     1.8    val source_explode: source -> Symbol_Pos.T list
     1.9    val source_content: source -> string
    1.10    val equal_content: source * source -> bool
    1.11 @@ -24,6 +25,9 @@
    1.12  abstype source = Source of {delimited: bool, text: Symbol_Pos.text, range: Position.range}
    1.13  with
    1.14  
    1.15 +
    1.16 +(* source *)
    1.17 +
    1.18  fun is_delimited (Source {delimited, ...}) = delimited;
    1.19  fun text_of (Source {text, ...}) = text;
    1.20  fun pos_of (Source {range = (pos, _), ...}) = pos;
    1.21 @@ -34,6 +38,11 @@
    1.22  
    1.23  fun string text = source true text Position.no_range;
    1.24  
    1.25 +fun reset_pos (Source {delimited, text, ...}) = source delimited text Position.no_range;
    1.26 +
    1.27 +
    1.28 +(* content *)
    1.29 +
    1.30  fun source_explode (Source {text, range = (pos, _), ...}) =
    1.31    Symbol_Pos.explode (text, pos);
    1.32  
    1.33 @@ -44,4 +53,3 @@
    1.34  end;
    1.35  
    1.36  end;
    1.37 -
     2.1 --- a/src/Pure/Syntax/mixfix.ML	Wed Mar 30 14:35:41 2016 +0200
     2.2 +++ b/src/Pure/Syntax/mixfix.ML	Wed Mar 30 14:52:23 2016 +0200
     2.3 @@ -25,6 +25,7 @@
     2.4    val set_range: Position.range -> mixfix -> mixfix
     2.5    val range_of: mixfix -> Position.range
     2.6    val pos_of: mixfix -> Position.T
     2.7 +  val reset_pos: mixfix -> mixfix
     2.8    val pretty_mixfix: mixfix -> Pretty.T
     2.9    val mixfix_args: mixfix -> int
    2.10    val mixfixT: mixfix -> typ
    2.11 @@ -86,6 +87,15 @@
    2.12  
    2.13  val pos_of = Position.set_range o range_of;
    2.14  
    2.15 +fun reset_pos NoSyn = NoSyn
    2.16 +  | reset_pos (Mixfix (sy, ps, p, _)) = Mixfix (Input.reset_pos sy, ps, p, Position.no_range)
    2.17 +  | reset_pos (Delimfix (sy, _)) = Delimfix (Input.reset_pos sy, Position.no_range)
    2.18 +  | reset_pos (Infix (sy, p, _)) = Infix (Input.reset_pos sy, p, Position.no_range)
    2.19 +  | reset_pos (Infixl (sy, p, _)) = Infixl (Input.reset_pos sy, p, Position.no_range)
    2.20 +  | reset_pos (Infixr (sy, p, _)) = Infixr (Input.reset_pos sy, p, Position.no_range)
    2.21 +  | reset_pos (Binder (sy, p, q, _)) = Binder (Input.reset_pos sy, p, q, Position.no_range)
    2.22 +  | reset_pos (Structure _) = Structure Position.no_range;
    2.23 +
    2.24  
    2.25  (* pretty_mixfix *)
    2.26