enable inner syntax source positions by default (controlled via configuration option);
disable source positions for HOLCF, due to special pattern translations;
--- 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)
--- 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 {*
--- 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 #>
--- 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;