equal
deleted
inserted
replaced
29 val show_markup_default: bool Unsynchronized.ref |
29 val show_markup_default: bool Unsynchronized.ref |
30 val show_markup_raw: Config.raw |
30 val show_markup_raw: Config.raw |
31 val show_structs_raw: Config.raw |
31 val show_structs_raw: Config.raw |
32 val show_question_marks_default: bool Unsynchronized.ref |
32 val show_question_marks_default: bool Unsynchronized.ref |
33 val show_question_marks_raw: Config.raw |
33 val show_question_marks_raw: Config.raw |
|
34 val show_type_constraint: Proof.context -> bool |
|
35 val show_sort_constraint: Proof.context -> bool |
34 type prtabs |
36 type prtabs |
35 val empty_prtabs: prtabs |
37 val empty_prtabs: prtabs |
36 val update_prtabs: string -> Syntax_Ext.xprod list -> prtabs -> prtabs |
38 val update_prtabs: string -> Syntax_Ext.xprod list -> prtabs -> prtabs |
37 val remove_prtabs: string -> Syntax_Ext.xprod list -> prtabs -> prtabs |
39 val remove_prtabs: string -> Syntax_Ext.xprod list -> prtabs -> prtabs |
38 val merge_prtabs: prtabs -> prtabs -> prtabs |
40 val merge_prtabs: prtabs -> prtabs -> prtabs |
77 |
79 |
78 val show_question_marks_default = Unsynchronized.ref true; |
80 val show_question_marks_default = Unsynchronized.ref true; |
79 val show_question_marks_raw = |
81 val show_question_marks_raw = |
80 Config.declare "show_question_marks" (fn _ => Config.Bool (! show_question_marks_default)); |
82 Config.declare "show_question_marks" (fn _ => Config.Bool (! show_question_marks_default)); |
81 val show_question_marks = Config.bool show_question_marks_raw; |
83 val show_question_marks = Config.bool show_question_marks_raw; |
|
84 |
|
85 fun show_type_constraint ctxt = Config.get ctxt show_types orelse Config.get ctxt show_markup; |
|
86 fun show_sort_constraint ctxt = Config.get ctxt show_sorts orelse Config.get ctxt show_markup; |
82 |
87 |
83 |
88 |
84 |
89 |
85 (** type prtabs **) |
90 (** type prtabs **) |
86 |
91 |