# HG changeset patch
# User wenzelm
# Date 1302123840 -7200
# Node ID b6c1b0c4c5114d9c7a1800bd2d7b97deedd0a67e
# Parent  49b1b8d0782f89ebacd4f78b0312cc5ec3708b37
separate structure Term_Position;
dismantled remains of structure Type_Ext;

diff -r 49b1b8d0782f -r b6c1b0c4c511 src/HOL/HOLCF/Cfun.thy
--- a/src/HOL/HOLCF/Cfun.thy	Wed Apr 06 22:25:44 2011 +0200
+++ b/src/HOL/HOLCF/Cfun.thy	Wed Apr 06 23:04:00 2011 +0200
@@ -57,7 +57,7 @@
   let
     fun Lambda_ast_tr [pats, body] =
           Ast.fold_ast_p @{syntax_const "_cabs"}
-            (Ast.unfold_ast @{syntax_const "_cargs"} (Syntax.strip_positions_ast pats), body)
+            (Ast.unfold_ast @{syntax_const "_cargs"} (Ast.strip_positions pats), body)
       | Lambda_ast_tr asts = raise Ast.AST ("Lambda_ast_tr", asts);
   in [(@{syntax_const "_Lambda"}, Lambda_ast_tr)] end;
 *}
diff -r 49b1b8d0782f -r b6c1b0c4c511 src/HOL/HOLCF/Tools/Domain/domain_constructors.ML
--- a/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML	Wed Apr 06 22:25:44 2011 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML	Wed Apr 06 23:04:00 2011 +0200
@@ -456,7 +456,7 @@
       fun con1 authentic n (con,args) =
           Library.foldl capp (c_ast authentic con, argvars n args)
       fun case1 authentic (n, c) =
-          app "_case1" (Syntax.strip_positions_ast (con1 authentic n c), expvar n)
+          app "_case1" (Ast.strip_positions (con1 authentic n c), expvar n)
       fun arg1 (n, (con,args)) = List.foldr cabs (expvar n) (argvars n args)
       fun when1 n (m, c) = if n = m then arg1 (n, c) else Ast.Constant @{const_syntax bottom}
       val case_constant = Ast.Constant (syntax (case_const dummyT))
diff -r 49b1b8d0782f -r b6c1b0c4c511 src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Apr 06 22:25:44 2011 +0200
+++ b/src/HOL/List.thy	Wed Apr 06 23:04:00 2011 +0200
@@ -385,7 +385,7 @@
     let
       val x = Free (Name.variant (fold Term.add_free_names [p, e] []) "x", dummyT);
       val e = if opti then singl e else e;
-      val case1 = Syntax.const @{syntax_const "_case1"} $ Syntax.strip_positions p $ e;
+      val case1 = Syntax.const @{syntax_const "_case1"} $ Term_Position.strip_positions p $ e;
       val case2 =
         Syntax.const @{syntax_const "_case1"} $
           Syntax.const @{const_syntax dummy_pattern} $ NilC;
diff -r 49b1b8d0782f -r b6c1b0c4c511 src/HOL/Statespace/state_space.ML
--- a/src/HOL/Statespace/state_space.ML	Wed Apr 06 22:25:44 2011 +0200
+++ b/src/HOL/Statespace/state_space.ML	Wed Apr 06 23:04:00 2011 +0200
@@ -624,7 +624,7 @@
            else raise TERM ("StateSpace.gen_lookup_tr: component " ^ n ^ " not defined",[]));
 
 fun lookup_tr ctxt [s, x] =
-  (case Syntax.strip_positions x of
+  (case Term_Position.strip_positions x of
     Free (n,_) => gen_lookup_tr ctxt s n
   | _ => raise Match);
 
@@ -656,7 +656,7 @@
    end;
 
 fun update_tr ctxt [s, x, v] =
-  (case Syntax.strip_positions x of
+  (case Term_Position.strip_positions x of
     Free (n, _) => gen_update_tr false ctxt n v s
   | _ => raise Match);
 
diff -r 49b1b8d0782f -r b6c1b0c4c511 src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Wed Apr 06 22:25:44 2011 +0200
+++ b/src/Pure/IsaMakefile	Wed Apr 06 23:04:00 2011 +0200
@@ -188,7 +188,7 @@
   Syntax/syn_trans.ML					\
   Syntax/syntax.ML					\
   Syntax/syntax_phases.ML				\
-  Syntax/type_ext.ML					\
+  Syntax/term_position.ML				\
   System/isabelle_process.ML				\
   System/isabelle_system.ML				\
   System/isar.ML					\
diff -r 49b1b8d0782f -r b6c1b0c4c511 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Wed Apr 06 22:25:44 2011 +0200
+++ b/src/Pure/ROOT.ML	Wed Apr 06 23:04:00 2011 +0200
@@ -114,16 +114,16 @@
 use "sorts.ML";
 use "type.ML";
 use "logic.ML";
-use "Syntax/lexicon.ML";
-use "Syntax/simple_syntax.ML";
 
 
 (* inner syntax *)
 
+use "Syntax/term_position.ML";
+use "Syntax/lexicon.ML";
+use "Syntax/simple_syntax.ML";
 use "Syntax/ast.ML";
 use "Syntax/syn_ext.ML";
 use "Syntax/parser.ML";
-use "Syntax/type_ext.ML";
 use "Syntax/syn_trans.ML";
 use "Syntax/mixfix.ML";
 use "Syntax/printer.ML";
diff -r 49b1b8d0782f -r b6c1b0c4c511 src/Pure/Syntax/ast.ML
--- a/src/Pure/Syntax/ast.ML	Wed Apr 06 22:25:44 2011 +0200
+++ b/src/Pure/Syntax/ast.ML	Wed Apr 06 23:04:00 2011 +0200
@@ -14,6 +14,7 @@
   exception AST of string * ast list
   val pretty_ast: ast -> Pretty.T
   val pretty_rule: ast * ast -> Pretty.T
+  val strip_positions: ast -> ast
   val head_of_rule: ast * ast -> string
   val rule_error: ast * ast -> string option
   val fold_ast: string -> ast list -> ast
@@ -57,8 +58,8 @@
 
 fun pretty_ast (Constant a) = Pretty.quote (Pretty.str a)
   | pretty_ast (Variable x) =
-      (case Lexicon.decode_position x of
-        SOME pos => Lexicon.pretty_position pos
+      (case Term_Position.decode x of
+        SOME pos => Term_Position.pretty pos
       | NONE => Pretty.str x)
   | pretty_ast (Appl asts) = Pretty.enclose "(" ")" (Pretty.breaks (map pretty_ast asts));
 
@@ -66,7 +67,17 @@
   Pretty.block [pretty_ast lhs, Pretty.str "  ->", Pretty.brk 2, pretty_ast rhs];
 
 
-(* head_of_ast, head_of_rule *)
+(* strip_positions *)
+
+fun strip_positions (Appl ((t as Constant c) :: u :: (v as Variable x) :: asts)) =
+      if (c = "_constrain" orelse c = "_constrainAbs") andalso is_some (Term_Position.decode x)
+      then mk_appl (strip_positions u) (map strip_positions asts)
+      else Appl (map strip_positions (t :: u :: v :: asts))
+  | strip_positions (Appl asts) = Appl (map strip_positions asts)
+  | strip_positions ast = ast;
+
+
+(* head_of_ast and head_of_rule *)
 
 fun head_of_ast (Constant a) = a
   | head_of_ast (Appl (Constant a :: _)) = a
diff -r 49b1b8d0782f -r b6c1b0c4c511 src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Wed Apr 06 22:25:44 2011 +0200
+++ b/src/Pure/Syntax/lexicon.ML	Wed Apr 06 23:04:00 2011 +0200
@@ -44,9 +44,6 @@
   val is_marked: string -> bool
   val dummy_type: term
   val fun_type: term
-  val pretty_position: Position.T -> Pretty.T
-  val encode_position: Position.T -> string
-  val decode_position: string -> Position.T option
 end;
 
 signature LEXICON =
@@ -459,24 +456,4 @@
     exp = length fracpart}
   end;
 
-
-(* positions *)
-
-val position_dummy = "<position>";
-val position_text = XML.Text position_dummy;
-
-fun pretty_position pos =
-  Pretty.markup (Position.markup pos Markup.position) [Pretty.str position_dummy];
-
-fun encode_position pos =
-  YXML.string_of (XML.Elem (Position.markup pos Markup.position, [position_text]));
-
-fun decode_position str =
-  (case YXML.parse_body str handle Fail msg => error msg of
-    [XML.Elem ((name, props), [arg])] =>
-      if name = Markup.positionN andalso arg = position_text
-      then SOME (Position.of_properties props)
-      else NONE
-  | _ => NONE);
-
 end;
diff -r 49b1b8d0782f -r b6c1b0c4c511 src/Pure/Syntax/syn_trans.ML
--- a/src/Pure/Syntax/syn_trans.ML	Wed Apr 06 22:25:44 2011 +0200
+++ b/src/Pure/Syntax/syn_trans.ML	Wed Apr 06 23:04:00 2011 +0200
@@ -86,7 +86,7 @@
 
 (* strip_positions *)
 
-fun strip_positions_ast_tr [ast] = Type_Ext.strip_positions_ast ast
+fun strip_positions_ast_tr [ast] = Ast.strip_positions ast
   | strip_positions_ast_tr asts = raise Ast.AST ("strip_positions_ast_tr", asts);
 
 
@@ -223,7 +223,7 @@
 fun update_name_tr (Free (x, T) :: ts) = list_comb (Free (suffix "_update" x, T), ts)
   | update_name_tr (Const (x, T) :: ts) = list_comb (Const (suffix "_update" x, T), ts)
   | update_name_tr (((c as Const ("_constrain", _)) $ t $ ty) :: ts) =
-      if Type_Ext.is_position ty then list_comb (c $ update_name_tr [t] $ ty, ts)
+      if Term_Position.is_position ty then list_comb (c $ update_name_tr [t] $ ty, ts)
       else
         list_comb (c $ update_name_tr [t] $
           (Lexicon.fun_type $
diff -r 49b1b8d0782f -r b6c1b0c4c511 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Wed Apr 06 22:25:44 2011 +0200
+++ b/src/Pure/Syntax/syntax.ML	Wed Apr 06 23:04:00 2011 +0200
@@ -16,7 +16,6 @@
 sig
   include LEXICON0
   include SYN_EXT0
-  include TYPE_EXT0
   include SYN_TRANS1
   include MIXFIX1
   include PRINTER0
@@ -795,7 +794,7 @@
 
 (*export parts of internal Syntax structures*)
 val syntax_tokenize = tokenize;
-open Lexicon Syn_Ext Type_Ext Syn_Trans Mixfix Printer;
+open Lexicon Syn_Ext Syn_Trans Mixfix Printer;
 val tokenize = syntax_tokenize;
 
 end;
@@ -804,6 +803,5 @@
 open Basic_Syntax;
 
 forget_structure "Syn_Ext";
-forget_structure "Type_Ext";
 forget_structure "Mixfix";
 
diff -r 49b1b8d0782f -r b6c1b0c4c511 src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Wed Apr 06 22:25:44 2011 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Wed Apr 06 23:04:00 2011 +0200
@@ -119,7 +119,7 @@
       | ast_of (Parser.Node ("_constrain_position", [pt as Parser.Tip tok])) =
           if constrain_pos then
             Ast.Appl [Ast.Constant "_constrain", ast_of pt,
-              Ast.Variable (Lexicon.encode_position (Lexicon.pos_of_token tok))]
+              Ast.Variable (Term_Position.encode (Lexicon.pos_of_token tok))]
           else ast_of pt
       | ast_of (Parser.Node (a, pts)) = trans a (map ast_of pts)
       | ast_of (Parser.Tip tok) = Ast.Variable (Lexicon.str_of_token tok);
@@ -172,11 +172,11 @@
         fun report ps = Position.reports reports ps;
 
         fun decode ps qs bs (Const ("_constrain", _) $ t $ typ) =
-              (case Syntax.decode_position_term typ of
+              (case Term_Position.decode_position typ of
                 SOME p => decode (p :: ps) qs bs t
               | NONE => Type.constraint (decodeT typ) (decode ps qs bs t))
           | decode ps qs bs (Const ("_constrainAbs", _) $ t $ typ) =
-              (case Syntax.decode_position_term typ of
+              (case Term_Position.decode_position typ of
                 SOME q => decode ps (q :: qs) bs t
               | NONE => Type.constraint (decodeT typ --> dummyT) (decode ps qs bs t))
           | decode _ qs bs (Abs (x, T, t)) =
@@ -418,7 +418,7 @@
     fun term_of (Type (a, Ts)) =
           Term.list_comb (Lexicon.const (Lexicon.mark_type a), map term_of Ts)
       | term_of (TFree (x, S)) =
-          if is_some (Lexicon.decode_position x) then Lexicon.free x
+          if is_some (Term_Position.decode x) then Lexicon.free x
           else of_sort (Lexicon.const "_tfree" $ Lexicon.free x) S
       | term_of (TVar (xi, S)) = of_sort (Lexicon.const "_tvar" $ Lexicon.var xi) S;
   in term_of ty end;
diff -r 49b1b8d0782f -r b6c1b0c4c511 src/Pure/Syntax/term_position.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Syntax/term_position.ML	Wed Apr 06 23:04:00 2011 +0200
@@ -0,0 +1,55 @@
+(*  Title:      Pure/Syntax/term_position.ML
+    Author:     Makarius
+
+Encoded position within term syntax trees.
+*)
+
+signature TERM_POSITION =
+sig
+  val pretty: Position.T -> Pretty.T
+  val encode: Position.T -> string
+  val decode: string -> Position.T option
+  val decode_position: term -> Position.T option
+  val is_position: term -> bool
+  val strip_positions: term -> term
+end;
+
+structure Term_Position: TERM_POSITION =
+struct
+
+(* markup *)
+
+val position_dummy = "<position>";
+val position_text = XML.Text position_dummy;
+
+fun pretty pos =
+  Pretty.markup (Position.markup pos Markup.position) [Pretty.str position_dummy];
+
+fun encode pos =
+  YXML.string_of (XML.Elem (Position.markup pos Markup.position, [position_text]));
+
+fun decode str =
+  (case YXML.parse_body str handle Fail msg => error msg of
+    [XML.Elem ((name, props), [arg])] =>
+      if name = Markup.positionN andalso arg = position_text
+      then SOME (Position.of_properties props)
+      else NONE
+  | _ => NONE);
+
+
+(* positions within parse trees *)
+
+fun decode_position (Free (x, _)) = decode x
+  | decode_position _ = NONE;
+
+val is_position = is_some o decode_position;
+
+fun strip_positions ((t as Const (c, _)) $ u $ v) =
+      if (c = "_constrain" orelse c = "_constrainAbs") andalso is_position v
+      then strip_positions u
+      else t $ strip_positions u $ strip_positions v
+  | strip_positions (t $ u) = strip_positions t $ strip_positions u
+  | strip_positions (Abs (x, T, t)) = Abs (x, T, strip_positions t)
+  | strip_positions t = t;
+
+end;
diff -r 49b1b8d0782f -r b6c1b0c4c511 src/Pure/Syntax/type_ext.ML
--- a/src/Pure/Syntax/type_ext.ML	Wed Apr 06 22:25:44 2011 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,47 +0,0 @@
-(*  Title:      Pure/Syntax/type_ext.ML
-    Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
-
-Utilities for input and output of types.  The concrete syntax of types.
-*)
-
-signature TYPE_EXT0 =
-sig
-  val decode_position_term: term -> Position.T option
-  val is_position: term -> bool
-  val strip_positions: term -> term
-  val strip_positions_ast: Ast.ast -> Ast.ast
-end;
-
-signature TYPE_EXT =
-sig
-  include TYPE_EXT0
-end;
-
-structure Type_Ext: TYPE_EXT =
-struct
-
-(** input utils **)
-
-(* positions *)
-
-fun decode_position_term (Free (x, _)) = Lexicon.decode_position x
-  | decode_position_term _ = NONE;
-
-val is_position = is_some o decode_position_term;
-
-fun strip_positions ((t as Const (c, _)) $ u $ v) =
-      if (c = "_constrain" orelse c = "_constrainAbs") andalso is_position v
-      then strip_positions u
-      else t $ strip_positions u $ strip_positions v
-  | strip_positions (t $ u) = strip_positions t $ strip_positions u
-  | strip_positions (Abs (x, T, t)) = Abs (x, T, strip_positions t)
-  | strip_positions t = t;
-
-fun strip_positions_ast (Ast.Appl ((t as Ast.Constant c) :: u :: (v as Ast.Variable x) :: asts)) =
-      if (c = "_constrain" orelse c = "_constrainAbs") andalso is_some (Lexicon.decode_position x)
-      then Ast.mk_appl (strip_positions_ast u) (map strip_positions_ast asts)
-      else Ast.Appl (map strip_positions_ast (t :: u :: v :: asts))
-  | strip_positions_ast (Ast.Appl asts) = Ast.Appl (map strip_positions_ast asts)
-  | strip_positions_ast ast = ast;
-
-end;