# HG changeset patch
# User wenzelm
# Date 1459342343 -7200
# Node ID d16b2ec535baab75977b9fcbd7f18257da225772
# Parent  c439a7348138196c2ae6d20390d0f40a439d40a6
more operations;

diff -r c439a7348138 -r d16b2ec535ba src/Pure/General/input.ML
--- a/src/Pure/General/input.ML	Wed Mar 30 14:35:41 2016 +0200
+++ b/src/Pure/General/input.ML	Wed Mar 30 14:52:23 2016 +0200
@@ -13,6 +13,7 @@
   val range_of: source -> Position.range
   val source: bool -> Symbol_Pos.text -> Position.range -> source
   val string: string -> source
+  val reset_pos: source -> source
   val source_explode: source -> Symbol_Pos.T list
   val source_content: source -> string
   val equal_content: source * source -> bool
@@ -24,6 +25,9 @@
 abstype source = Source of {delimited: bool, text: Symbol_Pos.text, range: Position.range}
 with
 
+
+(* source *)
+
 fun is_delimited (Source {delimited, ...}) = delimited;
 fun text_of (Source {text, ...}) = text;
 fun pos_of (Source {range = (pos, _), ...}) = pos;
@@ -34,6 +38,11 @@
 
 fun string text = source true text Position.no_range;
 
+fun reset_pos (Source {delimited, text, ...}) = source delimited text Position.no_range;
+
+
+(* content *)
+
 fun source_explode (Source {text, range = (pos, _), ...}) =
   Symbol_Pos.explode (text, pos);
 
@@ -44,4 +53,3 @@
 end;
 
 end;
-
diff -r c439a7348138 -r d16b2ec535ba src/Pure/Syntax/mixfix.ML
--- a/src/Pure/Syntax/mixfix.ML	Wed Mar 30 14:35:41 2016 +0200
+++ b/src/Pure/Syntax/mixfix.ML	Wed Mar 30 14:52:23 2016 +0200
@@ -25,6 +25,7 @@
   val set_range: Position.range -> mixfix -> mixfix
   val range_of: mixfix -> Position.range
   val pos_of: mixfix -> Position.T
+  val reset_pos: mixfix -> mixfix
   val pretty_mixfix: mixfix -> Pretty.T
   val mixfix_args: mixfix -> int
   val mixfixT: mixfix -> typ
@@ -86,6 +87,15 @@
 
 val pos_of = Position.set_range o range_of;
 
+fun reset_pos NoSyn = NoSyn
+  | reset_pos (Mixfix (sy, ps, p, _)) = Mixfix (Input.reset_pos sy, ps, p, Position.no_range)
+  | reset_pos (Delimfix (sy, _)) = Delimfix (Input.reset_pos sy, Position.no_range)
+  | reset_pos (Infix (sy, p, _)) = Infix (Input.reset_pos sy, p, Position.no_range)
+  | reset_pos (Infixl (sy, p, _)) = Infixl (Input.reset_pos sy, p, Position.no_range)
+  | reset_pos (Infixr (sy, p, _)) = Infixr (Input.reset_pos sy, p, Position.no_range)
+  | reset_pos (Binder (sy, p, q, _)) = Binder (Input.reset_pos sy, p, q, Position.no_range)
+  | reset_pos (Structure _) = Structure Position.no_range;
+
 
 (* pretty_mixfix *)