enable inner syntax source positions by default (controlled via configuration option);
authorwenzelm
Tue Mar 22 18:03:28 2011 +0100 (2011-03-22)
changeset 42056160a630b2c7e
parent 42055 ad87c485ff30
child 42057 3eba96ff3d3e
enable inner syntax source positions by default (controlled via configuration option);
disable source positions for HOLCF, due to special pattern translations;
NEWS
src/HOL/HOLCF/Cfun.thy
src/Pure/Isar/attrib.ML
src/Pure/Syntax/syntax.ML
     1.1 --- a/NEWS	Tue Mar 22 17:51:15 2011 +0100
     1.2 +++ b/NEWS	Tue Mar 22 18:03:28 2011 +0100
     1.3 @@ -71,6 +71,14 @@
     1.4  * Path.print is the official way to show file-system paths to users
     1.5  (including quotes etc.).
     1.6  
     1.7 +* Inner syntax: identifiers in parse trees of generic categories
     1.8 +"logic", "aprop", "idt" etc. carry position information (disguised as
     1.9 +type constraints).  Occasional INCOMPATIBILITY with non-compliant
    1.10 +translations that choke on unexpected type constraints: use
    1.11 +Syntax.strip_positions or Syntax.strip_positions_ast.  As last resort,
    1.12 +reset the configuration option Syntax.positions, which is called
    1.13 +"syntax_positions" in Isar attribute source.
    1.14 +
    1.15  
    1.16  
    1.17  New in Isabelle2011 (January 2011)
     2.1 --- a/src/HOL/HOLCF/Cfun.thy	Tue Mar 22 17:51:15 2011 +0100
     2.2 +++ b/src/HOL/HOLCF/Cfun.thy	Tue Mar 22 18:03:28 2011 +0100
     2.3 @@ -30,6 +30,8 @@
     2.4  
     2.5  subsection {* Syntax for continuous lambda abstraction *}
     2.6  
     2.7 +declare [[syntax_positions = false]]  (* FIXME pattern translations choke on position constraints *)
     2.8 +
     2.9  syntax "_cabs" :: "[logic, logic] \<Rightarrow> logic"
    2.10  
    2.11  parse_translation {*
     3.1 --- a/src/Pure/Isar/attrib.ML	Tue Mar 22 17:51:15 2011 +0100
     3.2 +++ b/src/Pure/Isar/attrib.ML	Tue Mar 22 18:03:28 2011 +0100
     3.3 @@ -400,6 +400,7 @@
     3.4  val _ = Context.>> (Context.map_theory
     3.5   (register_config Syntax.ast_trace_raw #>
     3.6    register_config Syntax.ast_stat_raw #>
     3.7 +  register_config Syntax.positions_raw #>
     3.8    register_config Syntax.show_brackets_raw #>
     3.9    register_config Syntax.show_sorts_raw #>
    3.10    register_config Syntax.show_types_raw #>
     4.1 --- a/src/Pure/Syntax/syntax.ML	Tue Mar 22 17:51:15 2011 +0100
     4.2 +++ b/src/Pure/Syntax/syntax.ML	Tue Mar 22 18:03:28 2011 +0100
     4.3 @@ -110,6 +110,8 @@
     4.4    val print_trans: syntax -> unit
     4.5    val print_syntax: syntax -> unit
     4.6    val guess_infix: syntax -> string -> mixfix option
     4.7 +  val positions_raw: Config.raw
     4.8 +  val positions: bool Config.T
     4.9    val ambiguity_enabled: bool Config.T
    4.10    val ambiguity_level_raw: Config.raw
    4.11    val ambiguity_level: int Config.T
    4.12 @@ -697,6 +699,9 @@
    4.13  
    4.14  (* read_ast *)
    4.15  
    4.16 +val positions_raw = Config.declare "syntax_positions" (fn _ => Config.Bool true);
    4.17 +val positions = Config.bool positions_raw;
    4.18 +
    4.19  val ambiguity_enabled =
    4.20    Config.bool (Config.declare "syntax_ambiguity_enabled" (fn _ => Config.Bool true));
    4.21  
    4.22 @@ -732,8 +737,10 @@
    4.23              "\nproduces " ^ string_of_int len ^ " parse trees" ^
    4.24              (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
    4.25              map show_pt (take limit pts))));
    4.26 +
    4.27 +    val constrain_pos = not raw andalso Config.get ctxt positions;
    4.28    in
    4.29 -    some_results (Syn_Trans.parsetree_to_ast ctxt false (lookup_tr parse_ast_trtab)) pts
    4.30 +    some_results (Syn_Trans.parsetree_to_ast ctxt constrain_pos (lookup_tr parse_ast_trtab)) pts
    4.31    end;
    4.32  
    4.33