discontinued Syntax.positions -- atomic parse trees are always annotated;
authorwenzelm
Thu Jan 05 20:26:01 2012 +0100 (2012-01-05)
changeset 46126bab00660539d
parent 46125 00cd193a48dc
child 46127 af3b95160b59
discontinued Syntax.positions -- atomic parse trees are always annotated;
NEWS
src/Pure/Isar/attrib.ML
src/Pure/Syntax/syntax.ML
src/Pure/Syntax/syntax_phases.ML
     1.1 --- a/NEWS	Thu Jan 05 18:18:39 2012 +0100
     1.2 +++ b/NEWS	Thu Jan 05 20:26:01 2012 +0100
     1.3 @@ -66,6 +66,9 @@
     1.4  pattern notation; e.g. see src/HOL/HOLCF/One.thy for translations of
     1.5  one_case.
     1.6  
     1.7 +* Discontinued configuration option "syntax_positions": atomic terms
     1.8 +in parse trees are always annotated by position constraints.
     1.9 +
    1.10  * Finite_Set.fold now qualified.  INCOMPATIBILITY.
    1.11  
    1.12  * Renamed some facts on canonical fold on lists, in order to avoid problems
     2.1 --- a/src/Pure/Isar/attrib.ML	Thu Jan 05 18:18:39 2012 +0100
     2.2 +++ b/src/Pure/Isar/attrib.ML	Thu Jan 05 20:26:01 2012 +0100
     2.3 @@ -498,7 +498,6 @@
     2.4  val _ = Context.>> (Context.map_theory
     2.5   (register_config Ast.trace_raw #>
     2.6    register_config Ast.stats_raw #>
     2.7 -  register_config Syntax.positions_raw #>
     2.8    register_config Printer.show_brackets_raw #>
     2.9    register_config Printer.show_sorts_raw #>
    2.10    register_config Printer.show_types_raw #>
     3.1 --- a/src/Pure/Syntax/syntax.ML	Thu Jan 05 18:18:39 2012 +0100
     3.2 +++ b/src/Pure/Syntax/syntax.ML	Thu Jan 05 20:26:01 2012 +0100
     3.3 @@ -10,8 +10,6 @@
     3.4    type operations
     3.5    val install_operations: operations -> unit
     3.6    val root: string Config.T
     3.7 -  val positions_raw: Config.raw
     3.8 -  val positions: bool Config.T
     3.9    val ambiguity_enabled: bool Config.T
    3.10    val ambiguity_level_raw: Config.raw
    3.11    val ambiguity_level: int Config.T
    3.12 @@ -159,9 +157,6 @@
    3.13  
    3.14  val root = Config.string (Config.declare "syntax_root" (K (Config.String "any")));
    3.15  
    3.16 -val positions_raw = Config.declare "syntax_positions" (fn _ => Config.Bool true);
    3.17 -val positions = Config.bool positions_raw;
    3.18 -
    3.19  val ambiguity_enabled =
    3.20    Config.bool (Config.declare "syntax_ambiguity_enabled" (fn _ => Config.Bool true));
    3.21  
     4.1 --- a/src/Pure/Syntax/syntax_phases.ML	Thu Jan 05 18:18:39 2012 +0100
     4.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Thu Jan 05 20:26:01 2012 +0100
     4.3 @@ -128,7 +128,7 @@
     4.4  
     4.5  (* parsetree_to_ast *)
     4.6  
     4.7 -fun parsetree_to_ast ctxt constrain_pos trf parsetree =
     4.8 +fun parsetree_to_ast ctxt raw trf parsetree =
     4.9    let
    4.10      val reports = Unsynchronized.ref ([]: Position.report list);
    4.11      fun report pos = Position.store_reports reports [pos];
    4.12 @@ -154,10 +154,10 @@
    4.13              val _ = report pos (markup_type ctxt) c;
    4.14            in [Ast.Constant (Lexicon.mark_type c)] end
    4.15        | asts_of (Parser.Node ("_position", [pt as Parser.Tip tok])) =
    4.16 -          if constrain_pos then
    4.17 +          if raw then [ast_of pt]
    4.18 +          else
    4.19              [Ast.Appl [Ast.Constant "_constrain", ast_of pt,
    4.20                Ast.Variable (Term_Position.encode (Lexicon.pos_of_token tok))]]
    4.21 -          else [ast_of pt]
    4.22        | asts_of (Parser.Node (a, pts)) =
    4.23            let
    4.24              val _ = pts |> List.app
    4.25 @@ -300,10 +300,9 @@
    4.26              (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
    4.27              map (Pretty.string_of o Parser.pretty_parsetree) (take limit pts))))
    4.28        else ();
    4.29 -
    4.30 -    val constrain_pos = not raw andalso Config.get ctxt Syntax.positions;
    4.31 -    val parsetree_to_ast = parsetree_to_ast ctxt constrain_pos ast_tr;
    4.32 -  in map parsetree_to_ast pts end;
    4.33 +  in
    4.34 +    map (parsetree_to_ast ctxt raw ast_tr) pts
    4.35 +  end;
    4.36  
    4.37  fun parse_raw ctxt root input =
    4.38    let