# HG changeset patch # User wenzelm # Date 1369686368 -7200 # Node ID c87b7f26e2c73cbbb41bc7b98ca72e8c2c6ac9cc # Parent d6627b50b131b7b523465891490132528258c429# Parent 816c88acd2698420ec39d3f4bbd0d30de292303d merged diff -r d6627b50b131 -r c87b7f26e2c7 src/HOL/Num.thy --- a/src/HOL/Num.thy Mon May 27 20:09:20 2013 +0200 +++ b/src/HOL/Num.thy Mon May 27 22:26:08 2013 +0200 @@ -326,14 +326,15 @@ fun num_tr' sign ctxt T [n] = let val k = dest_num n; - val t' = Syntax.const @{syntax_const "_Numeral"} $ - Syntax.free (sign ^ string_of_int k); + val t' = + Syntax.const @{syntax_const "_Numeral"} $ + Syntax.free (sign ^ string_of_int k); in (case T of Type (@{type_name fun}, [_, T']) => if not (Printer.show_type_constraint ctxt) andalso can Term.dest_Type T' then t' else Syntax.const @{syntax_const "_constrain"} $ t' $ Syntax_Phases.term_of_typ ctxt T' - | T' => if T' = dummyT then t' else raise Match) + | _ => if T = dummyT then t' else raise Match) end; in [(@{const_syntax numeral}, num_tr' ""), diff -r d6627b50b131 -r c87b7f26e2c7 src/Pure/Syntax/lexicon.ML --- a/src/Pure/Syntax/lexicon.ML Mon May 27 20:09:20 2013 +0200 +++ b/src/Pure/Syntax/lexicon.ML Mon May 27 22:26:08 2013 +0200 @@ -169,7 +169,9 @@ (* markup *) fun literal_markup s = - if Symbol.is_ascii_identifier s then Markup.literal else Markup.delimiter; + if Symbol.is_ascii_identifier s orelse exists Symbol.is_letter (Symbol.explode s) + then Markup.literal + else Markup.delimiter; val token_kind_markup = fn TFreeSy => Markup.tfree diff -r d6627b50b131 -r c87b7f26e2c7 src/Pure/Syntax/printer.ML --- a/src/Pure/Syntax/printer.ML Mon May 27 20:09:20 2013 +0200 +++ b/src/Pure/Syntax/printer.ML Mon May 27 22:26:08 2013 +0200 @@ -10,7 +10,6 @@ val show_types: bool Config.T val show_sorts: bool Config.T val show_free_types: bool Config.T - val show_all_types: bool Config.T val show_markup: bool Config.T val show_structs: bool Config.T val show_question_marks: bool Config.T @@ -60,7 +59,6 @@ val show_sorts = Config.bool show_sorts_raw; val show_free_types = Config.bool (Config.declare "show_free_types" (fn _ => Config.Bool true)); -val show_all_types = Config.bool (Config.declare "show_all_types" (fn _ => Config.Bool false)); val show_markup_default = Unsynchronized.ref false; val show_markup_raw = Config.declare "show_markup" (fn _ => Config.Bool (! show_markup_default)); diff -r d6627b50b131 -r c87b7f26e2c7 src/Pure/Syntax/syntax_phases.ML --- a/src/Pure/Syntax/syntax_phases.ML Mon May 27 20:09:20 2013 +0200 +++ b/src/Pure/Syntax/syntax_phases.ML Mon May 27 22:26:08 2013 +0200 @@ -136,7 +136,7 @@ (* parsetree_to_ast *) -fun parsetree_to_ast ctxt raw trf parsetree = +fun parsetree_to_ast ctxt trf parsetree = let val reports = Unsynchronized.ref ([]: Position.report list); fun report pos = Position.store_reports reports [pos]; @@ -155,12 +155,10 @@ Ast.Variable (Term_Position.encode (Lexicon.pos_of_token tok)); fun ast_of_dummy a tok = - if raw then Ast.Constant a - else Ast.Appl [Ast.Constant "_constrain", Ast.Constant a, ast_of_position tok]; + Ast.Appl [Ast.Constant "_constrain", Ast.Constant a, ast_of_position tok]; fun asts_of_position c tok = - if raw then asts_of_token tok - else [Ast.Appl [Ast.Constant c, ast_of (Parser.Tip tok), ast_of_position tok]] + [Ast.Appl [Ast.Constant c, ast_of (Parser.Tip tok), ast_of_position tok]] and asts_of (Parser.Node ("_class_name", [Parser.Tip tok])) = let @@ -322,7 +320,7 @@ (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") :: map (Pretty.string_of o Parser.pretty_parsetree) (take limit pts))]; - in (ambig_msgs, map (parsetree_to_ast ctxt raw ast_tr) pts) end; + in (ambig_msgs, map (parsetree_to_ast ctxt ast_tr) pts) end; fun parse_tree ctxt root input = let @@ -421,19 +419,32 @@ let val syn = Proof_Context.syn_of ctxt; - fun constify (ast as Ast.Constant _) = ast - | constify (ast as Ast.Variable x) = + val reports = Unsynchronized.ref ([]: Position.report list); + fun report ps = Position.store_reports reports ps; + + fun decode_const ps c = (report ps (markup_entity ctxt) c; Ast.Constant c); + fun decode_var ps x = (report ps (fn () => [Markup.name x Markup.free]) (); Ast.Variable x); + fun decode_appl ps asts = Ast.Appl (map (decode ps) asts) + and decode ps (Ast.Constant c) = decode_const ps c + | decode ps (Ast.Variable x) = if is_some (Syntax.lookup_const syn x) orelse Long_Name.is_qualified x - then Ast.Constant x - else ast - | constify (Ast.Appl asts) = Ast.Appl (map constify asts); + then decode_const ps x + else decode_var ps x + | decode ps (Ast.Appl (asts as (Ast.Constant c :: ast :: Ast.Variable x :: args))) = + if member (op =) Term_Position.markers c then + (case Term_Position.decode x of + SOME p => Ast.mk_appl (decode (p :: ps) ast) (map (decode ps) args) + | NONE => decode_appl ps asts) + else decode_appl ps asts + | decode ps (Ast.Appl asts) = decode_appl ps asts; val (syms, pos) = Syntax.read_token str; - in - parse_asts ctxt true root (syms, pos) - |> uncurry (report_result ctxt pos) - |> constify - end; + val ast = + parse_asts ctxt true root (syms, pos) + |> uncurry (report_result ctxt pos) + |> decode []; + val _ = Context_Position.reports ctxt (! reports); + in ast end; @@ -541,48 +552,43 @@ (mark Ts t1 $ mark Ts t2); in mark [] tm end; -in - -fun term_to_ast idents is_syntax_const ctxt trf tm = +fun prune_types ctxt tm = let - val show_types = - Config.get ctxt show_types orelse Config.get ctxt show_sorts orelse - Config.get ctxt show_all_types; - val show_structs = Config.get ctxt show_structs; val show_free_types = Config.get ctxt show_free_types; - val show_all_types = Config.get ctxt show_all_types; - val show_markup = Config.get ctxt show_markup; - val {structs, fixes} = idents; - - fun prune_typs (t_seen as (Const _, _)) = t_seen - | prune_typs (t as Free (x, ty), seen) = + fun prune (t_seen as (Const _, _)) = t_seen + | prune (t as Free (x, ty), seen) = if ty = dummyT then (t, seen) else if not show_free_types orelse member (op aconv) seen t then (Syntax.free x, seen) else (t, t :: seen) - | prune_typs (t as Var (xi, ty), seen) = + | prune (t as Var (xi, ty), seen) = if ty = dummyT then (t, seen) else if not show_free_types orelse member (op aconv) seen t then (Syntax.var xi, seen) else (t, t :: seen) - | prune_typs (t_seen as (Bound _, _)) = t_seen - | prune_typs (Abs (x, ty, t), seen) = - let val (t', seen') = prune_typs (t, seen); + | prune (t_seen as (Bound _, _)) = t_seen + | prune (Abs (x, ty, t), seen) = + let val (t', seen') = prune (t, seen); in (Abs (x, ty, t'), seen') end - | prune_typs (t1 $ t2, seen) = + | prune (t1 $ t2, seen) = let - val (t1', seen') = prune_typs (t1, seen); - val (t2', seen'') = prune_typs (t2, seen'); + val (t1', seen') = prune (t1, seen); + val (t2', seen'') = prune (t2, seen'); in (t1' $ t2', seen'') end; + in #1 (prune (tm, [])) end; - fun mark_atoms ((t as Const (c, _)) $ u) = +fun mark_atoms {structs, fixes} is_syntax_const ctxt tm = + let + val show_structs = Config.get ctxt show_structs; + + fun mark ((t as Const (c, _)) $ u) = if member (op =) Pure_Thy.token_markers c - then t $ u else mark_atoms t $ mark_atoms u - | mark_atoms (t $ u) = mark_atoms t $ mark_atoms u - | mark_atoms (Abs (x, T, t)) = Abs (x, T, mark_atoms t) - | mark_atoms (t as Const (c, T)) = + then t $ u else mark t $ mark u + | mark (t $ u) = mark t $ mark u + | mark (Abs (x, T, t)) = Abs (x, T, mark t) + | mark (t as Const (c, T)) = if is_syntax_const c then t else Const (Lexicon.mark_const c, T) - | mark_atoms (t as Free (x, T)) = + | mark (t as Free (x, T)) = let val i = find_index (fn s => s = x) structs + 1 in if i = 0 andalso member (op =) fixes x then Const (Lexicon.mark_fixed x, T) @@ -590,10 +596,18 @@ Syntax.const "_struct" $ Syntax.const "_indexdefault" else Syntax.const "_free" $ t end - | mark_atoms (t as Var (xi, T)) = + | mark (t as Var (xi, T)) = if xi = Syntax_Ext.dddot_indexname then Const ("_DDDOT", T) else Syntax.const "_var" $ t - | mark_atoms a = a; + | mark a = a; + in mark tm end; + +in + +fun term_to_ast idents is_syntax_const ctxt trf tm = + let + val show_types = Config.get ctxt show_types orelse Config.get ctxt show_sorts; + val show_markup = Config.get ctxt show_markup; fun ast_of tm = (case strip_comb tm of @@ -610,10 +624,7 @@ in Ast.mk_appl (constrain (c $ Syntax.free x) X) (map ast_of ts) end | (Const ("_idtdummy", T), ts) => Ast.mk_appl (constrain (Syntax.const "_idtdummy") T) (map ast_of ts) - | (const as Const (c, T), ts) => - if show_all_types - then Ast.mk_appl (constrain const T) (map ast_of ts) - else trans c T ts + | (const as Const (c, T), ts) => trans c T ts | (t, ts) => Ast.mk_appl (simple_ast_of ctxt t) (map ast_of ts)) and trans a T args = ast_of (trf a ctxt T args) @@ -627,8 +638,8 @@ in tm |> mark_aprop - |> show_types ? (#1 o prune_typs o rpair []) - |> mark_atoms + |> show_types ? prune_types ctxt + |> mark_atoms idents is_syntax_const ctxt |> ast_of end; @@ -666,9 +677,7 @@ let val show_markup = Config.get ctxt show_markup; val show_sorts = Config.get ctxt show_sorts; - val show_types = - Config.get ctxt show_types orelse show_sorts orelse - Config.get ctxt show_all_types; + val show_types = Config.get ctxt show_types orelse show_sorts; val syn = Proof_Context.syn_of ctxt; val prtabs = Syntax.prtabs syn; diff -r d6627b50b131 -r c87b7f26e2c7 src/Pure/goal_display.ML --- a/src/Pure/goal_display.ML Mon May 27 20:09:20 2013 +0200 +++ b/src/Pure/goal_display.ML Mon May 27 22:26:08 2013 +0200 @@ -71,10 +71,7 @@ let val ctxt = ctxt0 |> Config.put show_free_types false - |> Config.put show_types - (Config.get ctxt0 show_types orelse - Config.get ctxt0 show_sorts orelse - Config.get ctxt0 show_all_types) + |> Config.put show_types (Config.get ctxt0 show_types orelse Config.get ctxt0 show_sorts) |> Config.put show_sorts false; val show_sorts0 = Config.get ctxt0 show_sorts;