# HG changeset patch
# User wenzelm
# Date 1325791561 -3600
# Node ID bab00660539d88b7a80c51b423b0cd559396fc59
# Parent  00cd193a48dc142af3b166bddbd6278ca8ac14fe
discontinued Syntax.positions -- atomic parse trees are always annotated;

diff -r 00cd193a48dc -r bab00660539d NEWS
--- a/NEWS	Thu Jan 05 18:18:39 2012 +0100
+++ b/NEWS	Thu Jan 05 20:26:01 2012 +0100
@@ -66,6 +66,9 @@
 pattern notation; e.g. see src/HOL/HOLCF/One.thy for translations of
 one_case.
 
+* Discontinued configuration option "syntax_positions": atomic terms
+in parse trees are always annotated by position constraints.
+
 * Finite_Set.fold now qualified.  INCOMPATIBILITY.
 
 * Renamed some facts on canonical fold on lists, in order to avoid problems
diff -r 00cd193a48dc -r bab00660539d src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Thu Jan 05 18:18:39 2012 +0100
+++ b/src/Pure/Isar/attrib.ML	Thu Jan 05 20:26:01 2012 +0100
@@ -498,7 +498,6 @@
 val _ = Context.>> (Context.map_theory
  (register_config Ast.trace_raw #>
   register_config Ast.stats_raw #>
-  register_config Syntax.positions_raw #>
   register_config Printer.show_brackets_raw #>
   register_config Printer.show_sorts_raw #>
   register_config Printer.show_types_raw #>
diff -r 00cd193a48dc -r bab00660539d src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Thu Jan 05 18:18:39 2012 +0100
+++ b/src/Pure/Syntax/syntax.ML	Thu Jan 05 20:26:01 2012 +0100
@@ -10,8 +10,6 @@
   type operations
   val install_operations: operations -> unit
   val root: string Config.T
-  val positions_raw: Config.raw
-  val positions: bool Config.T
   val ambiguity_enabled: bool Config.T
   val ambiguity_level_raw: Config.raw
   val ambiguity_level: int Config.T
@@ -159,9 +157,6 @@
 
 val root = Config.string (Config.declare "syntax_root" (K (Config.String "any")));
 
-val positions_raw = Config.declare "syntax_positions" (fn _ => Config.Bool true);
-val positions = Config.bool positions_raw;
-
 val ambiguity_enabled =
   Config.bool (Config.declare "syntax_ambiguity_enabled" (fn _ => Config.Bool true));
 
diff -r 00cd193a48dc -r bab00660539d src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Thu Jan 05 18:18:39 2012 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML	Thu Jan 05 20:26:01 2012 +0100
@@ -128,7 +128,7 @@
 
 (* parsetree_to_ast *)
 
-fun parsetree_to_ast ctxt constrain_pos trf parsetree =
+fun parsetree_to_ast ctxt raw trf parsetree =
   let
     val reports = Unsynchronized.ref ([]: Position.report list);
     fun report pos = Position.store_reports reports [pos];
@@ -154,10 +154,10 @@
             val _ = report pos (markup_type ctxt) c;
           in [Ast.Constant (Lexicon.mark_type c)] end
       | asts_of (Parser.Node ("_position", [pt as Parser.Tip tok])) =
-          if constrain_pos then
+          if raw then [ast_of pt]
+          else
             [Ast.Appl [Ast.Constant "_constrain", ast_of pt,
               Ast.Variable (Term_Position.encode (Lexicon.pos_of_token tok))]]
-          else [ast_of pt]
       | asts_of (Parser.Node (a, pts)) =
           let
             val _ = pts |> List.app
@@ -300,10 +300,9 @@
             (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
             map (Pretty.string_of o Parser.pretty_parsetree) (take limit pts))))
       else ();
-
-    val constrain_pos = not raw andalso Config.get ctxt Syntax.positions;
-    val parsetree_to_ast = parsetree_to_ast ctxt constrain_pos ast_tr;
-  in map parsetree_to_ast pts end;
+  in
+    map (parsetree_to_ast ctxt raw ast_tr) pts
+  end;
 
 fun parse_raw ctxt root input =
   let