123 |
123 |
124 val value = Constant ""; |
124 val value = Constant ""; |
125 fun is_value (Constant "") = true |
125 fun is_value (Constant "") = true |
126 | is_value _ = false; |
126 | is_value _ = false; |
127 |
127 |
128 fun quote ctxt (Constant c) = Library.quote (Code.string_of_const (Proof_Context.theory_of ctxt) c) |
128 fun quote ctxt (Constant c) = |
129 | quote ctxt (Type_Constructor tyco) = "type " ^ Library.quote (Proof_Context.extern_type ctxt tyco) |
129 Library.quote (Code.string_of_const (Proof_Context.theory_of ctxt) c) |
130 | quote ctxt (Type_Class class) = "class " ^ Library.quote (Proof_Context.extern_class ctxt class) |
130 | quote ctxt (Type_Constructor tyco) = |
|
131 "type " ^ Library.quote (Proof_Context.markup_type ctxt tyco) |
|
132 | quote ctxt (Type_Class class) = |
|
133 "class " ^ Library.quote (Proof_Context.markup_class ctxt class) |
131 | quote ctxt (Class_Relation (sub, super)) = |
134 | quote ctxt (Class_Relation (sub, super)) = |
132 Library.quote (Proof_Context.extern_class ctxt sub) ^ " < " ^ Library.quote (Proof_Context.extern_class ctxt super) |
135 Library.quote (Proof_Context.markup_class ctxt sub) ^ " < " ^ |
|
136 Library.quote (Proof_Context.markup_class ctxt super) |
133 | quote ctxt (Class_Instance (tyco, class)) = |
137 | quote ctxt (Class_Instance (tyco, class)) = |
134 Library.quote (Proof_Context.extern_type ctxt tyco) ^ " :: " ^ Library.quote (Proof_Context.extern_class ctxt class); |
138 Library.quote (Proof_Context.markup_type ctxt tyco) ^ " :: " ^ |
|
139 Library.quote (Proof_Context.markup_class ctxt class); |
135 |
140 |
136 fun marker (Constant c) = "CONST " ^ c |
141 fun marker (Constant c) = "CONST " ^ c |
137 | marker (Type_Constructor tyco) = "TYPE " ^ tyco |
142 | marker (Type_Constructor tyco) = "TYPE " ^ tyco |
138 | marker (Type_Class class) = "CLASS " ^ class |
143 | marker (Type_Class class) = "CLASS " ^ class |
139 | marker (Class_Relation (sub, super)) = "CLASSREL " ^ sub ^ " < " ^ super |
144 | marker (Class_Relation (sub, super)) = "CLASSREL " ^ sub ^ " < " ^ super |