equal
deleted
inserted
replaced
49 |
49 |
50 fun markup_const ctxt c = |
50 fun markup_const ctxt c = |
51 [Name_Space.markup (Consts.space_of (Proof_Context.consts_of ctxt)) c]; |
51 [Name_Space.markup (Consts.space_of (Proof_Context.consts_of ctxt)) c]; |
52 |
52 |
53 fun markup_free ctxt x = |
53 fun markup_free ctxt x = |
54 (if Variable.is_improper ctxt x then Markup.improper |
54 Variable.markup ctxt x :: |
55 else if Name.is_skolem x then Markup.skolem |
|
56 else Markup.free) :: |
|
57 (if Variable.is_body ctxt orelse Variable.is_fixed ctxt x |
55 (if Variable.is_body ctxt orelse Variable.is_fixed ctxt x |
58 then [Variable.markup_fixed ctxt x] |
56 then [Variable.markup_fixed ctxt x] |
59 else []); |
57 else []); |
60 |
58 |
61 fun markup_var xi = [Markup.name (Term.string_of_vname xi) Markup.var]; |
59 fun markup_var xi = [Markup.name (Term.string_of_vname xi) Markup.var]; |