# HG changeset patch
# User wenzelm
# Date 1300813408 -3600
# Node ID 160a630b2c7ece0603dca3c15ae98d6cd812ff12
# Parent  ad87c485ff30022087fe1accf9e26b8b15707d7a
enable inner syntax source positions by default (controlled via configuration option);
disable source positions for HOLCF, due to special pattern translations;

diff -r ad87c485ff30 -r 160a630b2c7e NEWS
--- a/NEWS	Tue Mar 22 17:51:15 2011 +0100
+++ b/NEWS	Tue Mar 22 18:03:28 2011 +0100
@@ -71,6 +71,14 @@
 * Path.print is the official way to show file-system paths to users
 (including quotes etc.).
 
+* Inner syntax: identifiers in parse trees of generic categories
+"logic", "aprop", "idt" etc. carry position information (disguised as
+type constraints).  Occasional INCOMPATIBILITY with non-compliant
+translations that choke on unexpected type constraints: use
+Syntax.strip_positions or Syntax.strip_positions_ast.  As last resort,
+reset the configuration option Syntax.positions, which is called
+"syntax_positions" in Isar attribute source.
+
 
 
 New in Isabelle2011 (January 2011)
diff -r ad87c485ff30 -r 160a630b2c7e src/HOL/HOLCF/Cfun.thy
--- a/src/HOL/HOLCF/Cfun.thy	Tue Mar 22 17:51:15 2011 +0100
+++ b/src/HOL/HOLCF/Cfun.thy	Tue Mar 22 18:03:28 2011 +0100
@@ -30,6 +30,8 @@
 
 subsection {* Syntax for continuous lambda abstraction *}
 
+declare [[syntax_positions = false]]  (* FIXME pattern translations choke on position constraints *)
+
 syntax "_cabs" :: "[logic, logic] \<Rightarrow> logic"
 
 parse_translation {*
diff -r ad87c485ff30 -r 160a630b2c7e src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Tue Mar 22 17:51:15 2011 +0100
+++ b/src/Pure/Isar/attrib.ML	Tue Mar 22 18:03:28 2011 +0100
@@ -400,6 +400,7 @@
 val _ = Context.>> (Context.map_theory
  (register_config Syntax.ast_trace_raw #>
   register_config Syntax.ast_stat_raw #>
+  register_config Syntax.positions_raw #>
   register_config Syntax.show_brackets_raw #>
   register_config Syntax.show_sorts_raw #>
   register_config Syntax.show_types_raw #>
diff -r ad87c485ff30 -r 160a630b2c7e src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Tue Mar 22 17:51:15 2011 +0100
+++ b/src/Pure/Syntax/syntax.ML	Tue Mar 22 18:03:28 2011 +0100
@@ -110,6 +110,8 @@
   val print_trans: syntax -> unit
   val print_syntax: syntax -> unit
   val guess_infix: syntax -> string -> mixfix option
+  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
@@ -697,6 +699,9 @@
 
 (* read_ast *)
 
+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));
 
@@ -732,8 +737,10 @@
             "\nproduces " ^ string_of_int len ^ " parse trees" ^
             (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
             map show_pt (take limit pts))));
+
+    val constrain_pos = not raw andalso Config.get ctxt positions;
   in
-    some_results (Syn_Trans.parsetree_to_ast ctxt false (lookup_tr parse_ast_trtab)) pts
+    some_results (Syn_Trans.parsetree_to_ast ctxt constrain_pos (lookup_tr parse_ast_trtab)) pts
   end;