merged
authorwenzelm
Mon May 27 22:26:08 2013 +0200 (2013-05-27)
changeset 52190c87b7f26e2c7
parent 52184 d6627b50b131
parent 52189 816c88acd269
child 52191 636b62eb7e88
merged
     1.1 --- a/src/HOL/Num.thy	Mon May 27 20:09:20 2013 +0200
     1.2 +++ b/src/HOL/Num.thy	Mon May 27 22:26:08 2013 +0200
     1.3 @@ -326,14 +326,15 @@
     1.4      fun num_tr' sign ctxt T [n] =
     1.5        let
     1.6          val k = dest_num n;
     1.7 -        val t' = Syntax.const @{syntax_const "_Numeral"} $
     1.8 -          Syntax.free (sign ^ string_of_int k);
     1.9 +        val t' =
    1.10 +          Syntax.const @{syntax_const "_Numeral"} $
    1.11 +            Syntax.free (sign ^ string_of_int k);
    1.12        in
    1.13          (case T of
    1.14            Type (@{type_name fun}, [_, T']) =>
    1.15              if not (Printer.show_type_constraint ctxt) andalso can Term.dest_Type T' then t'
    1.16              else Syntax.const @{syntax_const "_constrain"} $ t' $ Syntax_Phases.term_of_typ ctxt T'
    1.17 -        | T' => if T' = dummyT then t' else raise Match)
    1.18 +        | _ => if T = dummyT then t' else raise Match)
    1.19        end;
    1.20    in
    1.21     [(@{const_syntax numeral}, num_tr' ""),
     2.1 --- a/src/Pure/Syntax/lexicon.ML	Mon May 27 20:09:20 2013 +0200
     2.2 +++ b/src/Pure/Syntax/lexicon.ML	Mon May 27 22:26:08 2013 +0200
     2.3 @@ -169,7 +169,9 @@
     2.4  (* markup *)
     2.5  
     2.6  fun literal_markup s =
     2.7 -  if Symbol.is_ascii_identifier s then Markup.literal else Markup.delimiter;
     2.8 +  if Symbol.is_ascii_identifier s orelse exists Symbol.is_letter (Symbol.explode s)
     2.9 +  then Markup.literal
    2.10 +  else Markup.delimiter;
    2.11  
    2.12  val token_kind_markup =
    2.13   fn TFreeSy => Markup.tfree
     3.1 --- a/src/Pure/Syntax/printer.ML	Mon May 27 20:09:20 2013 +0200
     3.2 +++ b/src/Pure/Syntax/printer.ML	Mon May 27 22:26:08 2013 +0200
     3.3 @@ -10,7 +10,6 @@
     3.4    val show_types: bool Config.T
     3.5    val show_sorts: bool Config.T
     3.6    val show_free_types: bool Config.T
     3.7 -  val show_all_types: bool Config.T
     3.8    val show_markup: bool Config.T
     3.9    val show_structs: bool Config.T
    3.10    val show_question_marks: bool Config.T
    3.11 @@ -60,7 +59,6 @@
    3.12  val show_sorts = Config.bool show_sorts_raw;
    3.13  
    3.14  val show_free_types = Config.bool (Config.declare "show_free_types" (fn _ => Config.Bool true));
    3.15 -val show_all_types = Config.bool (Config.declare "show_all_types" (fn _ => Config.Bool false));
    3.16  
    3.17  val show_markup_default = Unsynchronized.ref false;
    3.18  val show_markup_raw = Config.declare "show_markup" (fn _ => Config.Bool (! show_markup_default));
     4.1 --- a/src/Pure/Syntax/syntax_phases.ML	Mon May 27 20:09:20 2013 +0200
     4.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Mon May 27 22:26:08 2013 +0200
     4.3 @@ -136,7 +136,7 @@
     4.4  
     4.5  (* parsetree_to_ast *)
     4.6  
     4.7 -fun parsetree_to_ast ctxt raw trf parsetree =
     4.8 +fun parsetree_to_ast ctxt 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 @@ -155,12 +155,10 @@
    4.13        Ast.Variable (Term_Position.encode (Lexicon.pos_of_token tok));
    4.14  
    4.15      fun ast_of_dummy a tok =
    4.16 -      if raw then Ast.Constant a
    4.17 -      else Ast.Appl [Ast.Constant "_constrain", Ast.Constant a, ast_of_position tok];
    4.18 +      Ast.Appl [Ast.Constant "_constrain", Ast.Constant a, ast_of_position tok];
    4.19  
    4.20      fun asts_of_position c tok =
    4.21 -      if raw then asts_of_token tok
    4.22 -      else [Ast.Appl [Ast.Constant c, ast_of (Parser.Tip tok), ast_of_position tok]]
    4.23 +      [Ast.Appl [Ast.Constant c, ast_of (Parser.Tip tok), ast_of_position tok]]
    4.24  
    4.25      and asts_of (Parser.Node ("_class_name", [Parser.Tip tok])) =
    4.26            let
    4.27 @@ -322,7 +320,7 @@
    4.28              (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
    4.29              map (Pretty.string_of o Parser.pretty_parsetree) (take limit pts))];
    4.30  
    4.31 -  in (ambig_msgs, map (parsetree_to_ast ctxt raw ast_tr) pts) end;
    4.32 +  in (ambig_msgs, map (parsetree_to_ast ctxt ast_tr) pts) end;
    4.33  
    4.34  fun parse_tree ctxt root input =
    4.35    let
    4.36 @@ -421,19 +419,32 @@
    4.37    let
    4.38      val syn = Proof_Context.syn_of ctxt;
    4.39  
    4.40 -    fun constify (ast as Ast.Constant _) = ast
    4.41 -      | constify (ast as Ast.Variable x) =
    4.42 +    val reports = Unsynchronized.ref ([]: Position.report list);
    4.43 +    fun report ps = Position.store_reports reports ps;
    4.44 +
    4.45 +    fun decode_const ps c = (report ps (markup_entity ctxt) c; Ast.Constant c);
    4.46 +    fun decode_var ps x = (report ps (fn () => [Markup.name x Markup.free]) (); Ast.Variable x);
    4.47 +    fun decode_appl ps asts = Ast.Appl (map (decode ps) asts)
    4.48 +    and decode ps (Ast.Constant c) = decode_const ps c
    4.49 +      | decode ps (Ast.Variable x) =
    4.50            if is_some (Syntax.lookup_const syn x) orelse Long_Name.is_qualified x
    4.51 -          then Ast.Constant x
    4.52 -          else ast
    4.53 -      | constify (Ast.Appl asts) = Ast.Appl (map constify asts);
    4.54 +          then decode_const ps x
    4.55 +          else decode_var ps x
    4.56 +      | decode ps (Ast.Appl (asts as (Ast.Constant c :: ast :: Ast.Variable x :: args))) =
    4.57 +          if member (op =) Term_Position.markers c then
    4.58 +            (case Term_Position.decode x of
    4.59 +              SOME p => Ast.mk_appl (decode (p :: ps) ast) (map (decode ps) args)
    4.60 +            | NONE => decode_appl ps asts)
    4.61 +          else decode_appl ps asts
    4.62 +      | decode ps (Ast.Appl asts) = decode_appl ps asts;
    4.63  
    4.64      val (syms, pos) = Syntax.read_token str;
    4.65 -  in
    4.66 -    parse_asts ctxt true root (syms, pos)
    4.67 -    |> uncurry (report_result ctxt pos)
    4.68 -    |> constify
    4.69 -  end;
    4.70 +    val ast =
    4.71 +      parse_asts ctxt true root (syms, pos)
    4.72 +      |> uncurry (report_result ctxt pos)
    4.73 +      |> decode [];
    4.74 +    val _ = Context_Position.reports ctxt (! reports);
    4.75 +  in ast end;
    4.76  
    4.77  
    4.78  
    4.79 @@ -541,48 +552,43 @@
    4.80              (mark Ts t1 $ mark Ts t2);
    4.81    in mark [] tm end;
    4.82  
    4.83 -in
    4.84 -
    4.85 -fun term_to_ast idents is_syntax_const ctxt trf tm =
    4.86 +fun prune_types ctxt tm =
    4.87    let
    4.88 -    val show_types =
    4.89 -      Config.get ctxt show_types orelse Config.get ctxt show_sorts orelse
    4.90 -      Config.get ctxt show_all_types;
    4.91 -    val show_structs = Config.get ctxt show_structs;
    4.92      val show_free_types = Config.get ctxt show_free_types;
    4.93 -    val show_all_types = Config.get ctxt show_all_types;
    4.94 -    val show_markup = Config.get ctxt show_markup;
    4.95  
    4.96 -    val {structs, fixes} = idents;
    4.97 -
    4.98 -    fun prune_typs (t_seen as (Const _, _)) = t_seen
    4.99 -      | prune_typs (t as Free (x, ty), seen) =
   4.100 +    fun prune (t_seen as (Const _, _)) = t_seen
   4.101 +      | prune (t as Free (x, ty), seen) =
   4.102            if ty = dummyT then (t, seen)
   4.103            else if not show_free_types orelse member (op aconv) seen t then (Syntax.free x, seen)
   4.104            else (t, t :: seen)
   4.105 -      | prune_typs (t as Var (xi, ty), seen) =
   4.106 +      | prune (t as Var (xi, ty), seen) =
   4.107            if ty = dummyT then (t, seen)
   4.108            else if not show_free_types orelse member (op aconv) seen t then (Syntax.var xi, seen)
   4.109            else (t, t :: seen)
   4.110 -      | prune_typs (t_seen as (Bound _, _)) = t_seen
   4.111 -      | prune_typs (Abs (x, ty, t), seen) =
   4.112 -          let val (t', seen') = prune_typs (t, seen);
   4.113 +      | prune (t_seen as (Bound _, _)) = t_seen
   4.114 +      | prune (Abs (x, ty, t), seen) =
   4.115 +          let val (t', seen') = prune (t, seen);
   4.116            in (Abs (x, ty, t'), seen') end
   4.117 -      | prune_typs (t1 $ t2, seen) =
   4.118 +      | prune (t1 $ t2, seen) =
   4.119            let
   4.120 -            val (t1', seen') = prune_typs (t1, seen);
   4.121 -            val (t2', seen'') = prune_typs (t2, seen');
   4.122 +            val (t1', seen') = prune (t1, seen);
   4.123 +            val (t2', seen'') = prune (t2, seen');
   4.124            in (t1' $ t2', seen'') end;
   4.125 +  in #1 (prune (tm, [])) end;
   4.126  
   4.127 -    fun mark_atoms ((t as Const (c, _)) $ u) =
   4.128 +fun mark_atoms {structs, fixes} is_syntax_const ctxt tm =
   4.129 +  let
   4.130 +    val show_structs = Config.get ctxt show_structs;
   4.131 +
   4.132 +    fun mark ((t as Const (c, _)) $ u) =
   4.133            if member (op =) Pure_Thy.token_markers c
   4.134 -          then t $ u else mark_atoms t $ mark_atoms u
   4.135 -      | mark_atoms (t $ u) = mark_atoms t $ mark_atoms u
   4.136 -      | mark_atoms (Abs (x, T, t)) = Abs (x, T, mark_atoms t)
   4.137 -      | mark_atoms (t as Const (c, T)) =
   4.138 +          then t $ u else mark t $ mark u
   4.139 +      | mark (t $ u) = mark t $ mark u
   4.140 +      | mark (Abs (x, T, t)) = Abs (x, T, mark t)
   4.141 +      | mark (t as Const (c, T)) =
   4.142            if is_syntax_const c then t
   4.143            else Const (Lexicon.mark_const c, T)
   4.144 -      | mark_atoms (t as Free (x, T)) =
   4.145 +      | mark (t as Free (x, T)) =
   4.146            let val i = find_index (fn s => s = x) structs + 1 in
   4.147              if i = 0 andalso member (op =) fixes x then
   4.148                Const (Lexicon.mark_fixed x, T)
   4.149 @@ -590,10 +596,18 @@
   4.150                Syntax.const "_struct" $ Syntax.const "_indexdefault"
   4.151              else Syntax.const "_free" $ t
   4.152            end
   4.153 -      | mark_atoms (t as Var (xi, T)) =
   4.154 +      | mark (t as Var (xi, T)) =
   4.155            if xi = Syntax_Ext.dddot_indexname then Const ("_DDDOT", T)
   4.156            else Syntax.const "_var" $ t
   4.157 -      | mark_atoms a = a;
   4.158 +      | mark a = a;
   4.159 +  in mark tm end;
   4.160 +
   4.161 +in
   4.162 +
   4.163 +fun term_to_ast idents is_syntax_const ctxt trf tm =
   4.164 +  let
   4.165 +    val show_types = Config.get ctxt show_types orelse Config.get ctxt show_sorts;
   4.166 +    val show_markup = Config.get ctxt show_markup;
   4.167  
   4.168      fun ast_of tm =
   4.169        (case strip_comb tm of
   4.170 @@ -610,10 +624,7 @@
   4.171            in Ast.mk_appl (constrain (c $ Syntax.free x) X) (map ast_of ts) end
   4.172        | (Const ("_idtdummy", T), ts) =>
   4.173            Ast.mk_appl (constrain (Syntax.const "_idtdummy") T) (map ast_of ts)
   4.174 -      | (const as Const (c, T), ts) =>
   4.175 -          if show_all_types
   4.176 -          then Ast.mk_appl (constrain const T) (map ast_of ts)
   4.177 -          else trans c T ts
   4.178 +      | (const as Const (c, T), ts) => trans c T ts
   4.179        | (t, ts) => Ast.mk_appl (simple_ast_of ctxt t) (map ast_of ts))
   4.180  
   4.181      and trans a T args = ast_of (trf a ctxt T args)
   4.182 @@ -627,8 +638,8 @@
   4.183    in
   4.184      tm
   4.185      |> mark_aprop
   4.186 -    |> show_types ? (#1 o prune_typs o rpair [])
   4.187 -    |> mark_atoms
   4.188 +    |> show_types ? prune_types ctxt
   4.189 +    |> mark_atoms idents is_syntax_const ctxt
   4.190      |> ast_of
   4.191    end;
   4.192  
   4.193 @@ -666,9 +677,7 @@
   4.194    let
   4.195      val show_markup = Config.get ctxt show_markup;
   4.196      val show_sorts = Config.get ctxt show_sorts;
   4.197 -    val show_types =
   4.198 -      Config.get ctxt show_types orelse show_sorts orelse
   4.199 -      Config.get ctxt show_all_types;
   4.200 +    val show_types = Config.get ctxt show_types orelse show_sorts;
   4.201  
   4.202      val syn = Proof_Context.syn_of ctxt;
   4.203      val prtabs = Syntax.prtabs syn;
     5.1 --- a/src/Pure/goal_display.ML	Mon May 27 20:09:20 2013 +0200
     5.2 +++ b/src/Pure/goal_display.ML	Mon May 27 22:26:08 2013 +0200
     5.3 @@ -71,10 +71,7 @@
     5.4    let
     5.5      val ctxt = ctxt0
     5.6        |> Config.put show_free_types false
     5.7 -      |> Config.put show_types
     5.8 -       (Config.get ctxt0 show_types orelse
     5.9 -        Config.get ctxt0 show_sorts orelse
    5.10 -        Config.get ctxt0 show_all_types)
    5.11 +      |> Config.put show_types (Config.get ctxt0 show_types orelse Config.get ctxt0 show_sorts)
    5.12        |> Config.put show_sorts false;
    5.13  
    5.14      val show_sorts0 = Config.get ctxt0 show_sorts;