# HG changeset patch # User wenzelm # Date 1301255050 -7200 # Node ID f667e64a5b4db5fc0da45a827018d1155bfaff16 # Parent e54a985daa6152623682018c77a57aa7a29fd4e9# Parent 826168ae02132c2022c21c5aec2947e4322a6168 merged diff -r e54a985daa61 -r f667e64a5b4d src/Pure/General/markup.ML --- a/src/Pure/General/markup.ML Sun Mar 27 17:32:25 2011 +0200 +++ b/src/Pure/General/markup.ML Sun Mar 27 21:44:10 2011 +0200 @@ -16,7 +16,7 @@ val name: string -> T -> T val kindN: string val bindingN: string val binding: string -> T - val entityN: string val entity: string -> T + val entityN: string val entity: string -> string -> T val defN: string val refN: string val lineN: string @@ -174,7 +174,9 @@ (* formal entities *) val (bindingN, binding) = markup_string "binding" nameN; -val (entityN, entity) = markup_string "entity" nameN; + +val entityN = "entity"; +fun entity kind name = (entityN, [(kindN, kind), (nameN, name)]); val defN = "def"; val refN = "ref"; @@ -218,7 +220,7 @@ val (fixed_declN, fixed_decl) = markup_string "fixed_decl" nameN; val (fixedN, fixed) = markup_string "fixed" nameN; val (const_declN, const_decl) = markup_string "const_decl" nameN; -val (constN, const) = markup_string "const" nameN; +val (constN, const) = markup_string "constant" nameN; val (fact_declN, fact_decl) = markup_string "fact_decl" nameN; val (factN, fact) = markup_string "fact" nameN; val (dynamic_factN, dynamic_fact) = markup_string "dynamic_fact" nameN; diff -r e54a985daa61 -r f667e64a5b4d src/Pure/General/markup.scala --- a/src/Pure/General/markup.scala Sun Mar 27 17:32:25 2011 +0200 +++ b/src/Pure/General/markup.scala Sun Mar 27 21:44:10 2011 +0200 @@ -84,7 +84,10 @@ /* misc properties */ val NAME = "name" + val Name = new Property(NAME) + val KIND = "kind" + val Kind = new Property(KIND) /* formal entities */ @@ -129,7 +132,7 @@ val FIXED_DECL = "fixed_decl" val FIXED = "fixed" val CONST_DECL = "const_decl" - val CONST = "const" + val CONST = "constant" val FACT_DECL = "fact_decl" val FACT = "fact" val DYNAMIC_FACT = "dynamic_fact" diff -r e54a985daa61 -r f667e64a5b4d src/Pure/General/name_space.ML --- a/src/Pure/General/name_space.ML Sun Mar 27 17:32:25 2011 +0200 +++ b/src/Pure/General/name_space.ML Sun Mar 27 21:44:10 2011 +0200 @@ -24,6 +24,7 @@ val kind_of: T -> string val the_entry: T -> string -> {concealed: bool, group: serial option, theory_name: string, pos: Position.T, id: serial} + val markup_entry: T -> string -> Markup.T val is_concealed: T -> string -> bool val intern: T -> xstring -> string val extern_flags: {long_names: bool, short_names: bool, unique_names: bool} -> @@ -79,15 +80,18 @@ pos: Position.T, id: serial}; -fun str_of_entry def (name, {pos, id, ...}: entry) = +fun entry_markup def kind (name, {pos, id, ...}: entry) = let val occurrence = (if def then Markup.defN else Markup.refN, string_of_int id); val props = occurrence :: Position.properties_of pos; - in Markup.markup (Markup.properties props (Markup.entity name)) name end; + in Markup.properties props (Markup.entity kind name) end; + +fun print_entry def kind (name, entry) = + quote (Markup.markup (entry_markup def kind (name, entry)) name); fun err_dup kind entry1 entry2 = error ("Duplicate " ^ kind ^ " declaration " ^ - quote (str_of_entry true entry1) ^ " vs. " ^ quote (str_of_entry true entry2)); + print_entry true kind entry1 ^ " vs. " ^ print_entry true kind entry2); (* datatype T *) @@ -117,6 +121,11 @@ NONE => error ("Unknown " ^ kind ^ " " ^ quote name) | SOME (_, entry) => entry); +fun markup_entry (Name_Space {kind, entries, ...}) name = + (case Symtab.lookup entries name of + NONE => Markup.malformed + | SOME (_, entry) => entry_markup false kind (name, entry)); + fun is_concealed space name = #concealed (the_entry space name); diff -r e54a985daa61 -r f667e64a5b4d src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Sun Mar 27 17:32:25 2011 +0200 +++ b/src/Pure/Isar/proof_context.ML Sun Mar 27 21:44:10 2011 +0200 @@ -65,7 +65,7 @@ val allow_dummies: Proof.context -> Proof.context val check_tvar: Proof.context -> indexname * sort -> indexname * sort val check_tfree: Proof.context -> string * sort -> string * sort - val decode_term: Proof.context -> term -> term + val decode_term: Proof.context -> term -> (Position.T * Markup.T) list * term val standard_infer_types: Proof.context -> term list -> term list val read_term_pattern: Proof.context -> string -> term val read_term_schematic: Proof.context -> string -> term @@ -261,6 +261,7 @@ fun default_sort ctxt = the_default (Type.defaultS (tsig_of ctxt)) o Variable.def_sort ctxt; val consts_of = #1 o #consts o rep_context; +val const_space = Consts.space_of o consts_of; val the_const_constraint = Consts.the_constraint o consts_of; val facts_of = #facts o rep_context; @@ -664,15 +665,16 @@ in -fun term_context ctxt = - {get_sort = get_sort ctxt, - map_const = fn a => ((true, #1 (Term.dest_Const (read_const_proper ctxt false a))) - handle ERROR _ => (false, Consts.intern (consts_of ctxt) a)), - map_free = intern_skolem ctxt (Variable.def_type ctxt false)}; +fun term_context ctxt : Syntax.term_context = + {get_sort = get_sort ctxt, + get_const = fn a => ((true, #1 (Term.dest_Const (read_const_proper ctxt false a))) + handle ERROR _ => (false, Consts.intern (consts_of ctxt) a)), + get_free = intern_skolem ctxt (Variable.def_type ctxt false), + markup_const = Name_Space.markup_entry (const_space ctxt), + markup_free = fn x => Markup.name x Markup.free, + markup_var = fn xi => Markup.name (Term.string_of_vname xi) Markup.var}; -fun decode_term ctxt = - let val {get_sort, map_const, map_free} = term_context ctxt - in Syntax.decode_term get_sort map_const map_free end; +val decode_term = Syntax.decode_term o term_context; end; @@ -757,8 +759,6 @@ fun parse_term T ctxt text = let - val {get_sort, map_const, map_free} = term_context ctxt; - val (T', _) = Type_Infer.paramify_dummies T 0; val (markup, kind) = if T' = propT then (Markup.prop, "proposition") else (Markup.term, "term"); @@ -775,9 +775,8 @@ fun check t = (Syntax.check_term ctxt (Type.constraint T' t); NONE) handle ERROR msg => SOME msg; val t = - Syntax.standard_parse_term check get_sort map_const map_free - ctxt (syn_of ctxt) root (syms, pos) - handle ERROR msg => parse_failed ctxt pos msg kind; + Syntax.standard_parse_term check (term_context ctxt) ctxt (syn_of ctxt) root (syms, pos) + handle ERROR msg => parse_failed ctxt pos msg kind; in t end; diff -r e54a985daa61 -r f667e64a5b4d src/Pure/Syntax/mixfix.ML --- a/src/Pure/Syntax/mixfix.ML Sun Mar 27 17:32:25 2011 +0200 +++ b/src/Pure/Syntax/mixfix.ML Sun Mar 27 21:44:10 2011 +0200 @@ -109,7 +109,7 @@ | mfix_of (t, ty, Infix (sy, p)) = SOME (mk_infix sy ty t (p + 1) (p + 1) p) | mfix_of (t, ty, Infixl (sy, p)) = SOME (mk_infix sy ty t p (p + 1) p) | mfix_of (t, ty, Infixr (sy, p)) = SOME (mk_infix sy ty t (p + 1) p p) - | mfix_of (t, _, _) = error ("Bad mixfix declaration for " ^ quote t); (* FIXME printable t (!?) *) + | mfix_of (t, _, _) = error ("Bad mixfix declaration for " ^ quote t); fun check_args (_, ty, _) (SOME (mfix as Syn_Ext.Mfix (sy, _, _, _, _))) = if length (Term.binder_types ty) = Syn_Ext.mfix_args sy then () @@ -145,7 +145,7 @@ | mfix_of (c, ty, Infixr (sy, p)) = mk_infix sy ty c (p + 1) p p | mfix_of (c, ty, Binder (sy, p, q)) = [Syn_Ext.Mfix ("(3" ^ sy ^ "_./ _)", binder_typ c ty, (binder_name c), [0, p], q)] - | mfix_of (c, _, _) = error ("Bad mixfix declaration for " ^ quote c); (* FIXME printable c (!?) *) + | mfix_of (c, _, _) = error ("Bad mixfix declaration for " ^ quote c); fun binder (c, _, Binder _) = SOME (binder_name c, c) | binder _ = NONE; diff -r e54a985daa61 -r f667e64a5b4d src/Pure/Syntax/syntax.ML --- a/src/Pure/Syntax/syntax.ML Sun Mar 27 17:32:25 2011 +0200 +++ b/src/Pure/Syntax/syntax.ML Sun Mar 27 21:44:10 2011 +0200 @@ -116,10 +116,8 @@ val ambiguity_level_raw: Config.raw val ambiguity_level: int Config.T val ambiguity_limit: int Config.T - val standard_parse_term: (term -> string option) -> - (((string * int) * sort) list -> string * int -> Term.sort) -> - (string -> bool * string) -> (string -> string option) -> Proof.context -> - syntax -> string -> Symbol_Pos.T list * Position.T -> term + val standard_parse_term: (term -> string option) -> term_context -> + Proof.context -> syntax -> string -> Symbol_Pos.T list * Position.T -> term val standard_parse_typ: Proof.context -> syntax -> ((indexname * sort) list -> indexname -> sort) -> Symbol_Pos.T list * Position.T -> typ val standard_parse_sort: Proof.context -> syntax -> Symbol_Pos.T list * Position.T -> sort @@ -756,22 +754,25 @@ (* read terms *) +fun report_result ctxt (reports, res) = + (List.app (fn (pos, m) => Context_Position.report ctxt pos m) reports; res); + (*brute-force disambiguation via type-inference*) -fun disambig _ _ [t] = t - | disambig ctxt check ts = +fun disambig ctxt _ [arg] = report_result ctxt arg + | disambig ctxt check args = let val level = Config.get ctxt ambiguity_level; val limit = Config.get ctxt ambiguity_limit; - val ambiguity = length ts; + val ambiguity = length args; fun ambig_msg () = if ambiguity > 1 andalso ambiguity <= level then "Got more than one parse tree.\n\ \Retry with smaller syntax_ambiguity_level for more information." else ""; - val errs = Par_List.map_name "Syntax.disambig" check ts; - val results = map_filter (fn (t, NONE) => SOME t | _ => NONE) (ts ~~ errs); + val errs = Par_List.map_name "Syntax.disambig" (check o snd) args; + val results = map_filter (fn (arg, NONE) => SOME arg | _ => NONE) (args ~~ errs); val len = length results; val show_term = string_of_term (Config.put Printer.show_brackets true ctxt); @@ -782,16 +783,16 @@ Context_Position.if_visible ctxt warning "Fortunately, only one parse tree is type correct.\n\ \You may still want to disambiguate your grammar or your input." - else (); hd results) + else (); report_result ctxt (hd results)) else cat_error (ambig_msg ()) (cat_lines (("Ambiguous input, " ^ string_of_int len ^ " terms are type correct" ^ (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") :: - map show_term (take limit results))) + map (show_term o snd) (take limit results))) end; -fun standard_parse_term check get_sort map_const map_free ctxt syn root (syms, pos) = +fun standard_parse_term check term_ctxt ctxt syn root (syms, pos) = read ctxt syn root (syms, pos) - |> map (Type_Ext.decode_term get_sort map_const map_free) + |> map (Type_Ext.decode_term term_ctxt) |> disambig ctxt check; diff -r e54a985daa61 -r f667e64a5b4d src/Pure/Syntax/type_ext.ML --- a/src/Pure/Syntax/type_ext.ML Sun Mar 27 17:32:25 2011 +0200 +++ b/src/Pure/Syntax/type_ext.ML Sun Mar 27 21:44:10 2011 +0200 @@ -12,8 +12,8 @@ val is_position: term -> bool val strip_positions: term -> term val strip_positions_ast: Ast.ast -> Ast.ast - val decode_term: (((string * int) * sort) list -> string * int -> sort) -> - (string -> bool * string) -> (string -> string option) -> term -> term + type term_context + val decode_term: term_context -> term -> (Position.T * Markup.T) list * term val term_of_typ: bool -> typ -> term val no_brackets: unit -> bool val no_type_brackets: unit -> bool @@ -106,8 +106,10 @@ (* positions *) -fun is_position (Free (x, _)) = is_some (Lexicon.decode_position x) - | is_position _ = false; +fun decode_position (Free (x, _)) = Lexicon.decode_position x + | decode_position _ = NONE; + +val is_position = is_some o decode_position; fun strip_positions ((t as Const (c, _)) $ u $ v) = if (c = "_constrain" orelse c = "_constrainAbs") andalso is_position v @@ -127,35 +129,69 @@ (* decode_term -- transform parse tree into raw term *) -fun decode_term get_sort map_const map_free tm = +fun markup_bound def id = + Markup.properties [(if def then Markup.defN else Markup.refN, id)] Markup.bound; + +type term_context = + {get_sort: (indexname * sort) list -> indexname -> sort, + get_const: string -> bool * string, + get_free: string -> string option, + markup_const: string -> Markup.T, + markup_free: string -> Markup.T, + markup_var: indexname -> Markup.T}; + +fun decode_term (term_context: term_context) tm = let + val {get_sort, get_const, get_free, markup_const, markup_free, markup_var} = term_context; val decodeT = typ_of_term (get_sort (term_sorts tm)); - fun decode (Const ("_constrain", _) $ t $ typ) = - if is_position typ then decode t - else Type.constraint (decodeT typ) (decode t) - | decode (Const ("_constrainAbs", _) $ t $ typ) = - if is_position typ then decode t - else Type.constraint (decodeT typ --> dummyT) (decode t) - | decode (Abs (x, T, t)) = Abs (x, T, decode t) - | decode (t $ u) = decode t $ decode u - | decode (Const (a, T)) = + val reports = Unsynchronized.ref ([]: (Position.T * Markup.T) list); + fun report [] _ _ = () + | report ps markup x = + let val m = markup x + in Unsynchronized.change reports (fold (fn p => cons (p, m)) ps) end; + + fun decode ps qs bs (Const ("_constrain", _) $ t $ typ) = + (case decode_position typ of + SOME p => decode (p :: ps) qs bs t + | NONE => Type.constraint (decodeT typ) (decode ps qs bs t)) + | decode ps qs bs (Const ("_constrainAbs", _) $ t $ typ) = + (case decode_position typ of + SOME q => decode ps (q :: qs) bs t + | NONE => Type.constraint (decodeT typ --> dummyT) (decode ps qs bs t)) + | decode _ qs bs (Abs (x, T, t)) = + let + val id = serial_string (); + val _ = report qs (markup_bound true) id; + in Abs (x, T, decode [] [] (id :: bs) t) end + | decode _ _ bs (t $ u) = decode [] [] bs t $ decode [] [] bs u + | decode ps _ _ (Const (a, T)) = (case try Lexicon.unmark_fixed a of - SOME x => Free (x, T) + SOME x => (report ps markup_free x; Free (x, T)) | NONE => - let val c = - (case try Lexicon.unmark_const a of - SOME c => c - | NONE => snd (map_const a)) + let + val c = + (case try Lexicon.unmark_const a of + SOME c => c + | NONE => snd (get_const a)); + val _ = report ps markup_const c; in Const (c, T) end) - | decode (Free (a, T)) = - (case (map_free a, map_const a) of - (SOME x, _) => Free (x, T) - | (_, (true, c)) => Const (c, T) - | (_, (false, c)) => (if Long_Name.is_qualified c then Const else Free) (c, T)) - | decode (Var (xi, T)) = Var (xi, T) - | decode (t as Bound _) = t; - in decode tm end; + | decode ps _ _ (Free (a, T)) = + (case (get_free a, get_const a) of + (SOME x, _) => (report ps markup_free x; Free (x, T)) + | (_, (true, c)) => (report ps markup_const c; Const (c, T)) + | (_, (false, c)) => + if Long_Name.is_qualified c + then (report ps markup_const c; Const (c, T)) + else (report ps markup_free c; Free (c, T))) + | decode ps _ _ (Var (xi, T)) = (report ps markup_var xi; Var (xi, T)) + | decode ps _ bs (t as Bound i) = + (case try (nth bs) i of + SOME id => (report ps (markup_bound false) id; t) + | NONE => t); + + val tm' = decode [] [] [] tm; + in (! reports, tm') end; diff -r e54a985daa61 -r f667e64a5b4d src/Tools/jEdit/src/jedit/isabelle_markup.scala --- a/src/Tools/jEdit/src/jedit/isabelle_markup.scala Sun Mar 27 17:32:25 2011 +0200 +++ b/src/Tools/jEdit/src/jedit/isabelle_markup.scala Sun Mar 27 21:44:10 2011 +0200 @@ -144,7 +144,7 @@ Markup.FIXED_DECL -> FUNCTION, Markup.FIXED -> NULL, Markup.CONST_DECL -> FUNCTION, - Markup.CONST -> NULL, + Markup.CONST -> LITERAL2, Markup.FACT_DECL -> FUNCTION, Markup.FACT -> NULL, Markup.DYNAMIC_FACT -> LABEL, @@ -152,10 +152,10 @@ Markup.LOCAL_FACT -> NULL, // inner syntax Markup.TFREE -> NULL, - Markup.FREE -> NULL, + Markup.FREE -> MARKUP, Markup.TVAR -> NULL, Markup.SKOLEM -> NULL, - Markup.BOUND -> NULL, + Markup.BOUND -> LABEL, Markup.VAR -> NULL, Markup.NUM -> DIGIT, Markup.FLOAT -> DIGIT, @@ -204,6 +204,9 @@ case Text.Info(_, XML.Elem(Markup(Markup.COMMAND, List((Markup.NAME, name))), _)) if syntax.keyword_kind(name).isDefined => command_style(syntax.keyword_kind(name).get) + case Text.Info(_, XML.Elem(Markup(Markup.ENTITY, Markup.Kind(kind)), _)) + if token_style(kind) != Token.NULL => token_style(kind) + case Text.Info(_, XML.Elem(Markup(name, _), _)) if token_style(name) != Token.NULL => token_style(name) }