--- a/src/Pure/Syntax/printer.ML Wed Oct 03 16:59:20 2012 +0200
+++ b/src/Pure/Syntax/printer.ML Wed Oct 03 16:59:58 2012 +0200
@@ -31,6 +31,8 @@
val show_structs_raw: Config.raw
val show_question_marks_default: bool Unsynchronized.ref
val show_question_marks_raw: Config.raw
+ val show_type_constraint: Proof.context -> bool
+ val show_sort_constraint: Proof.context -> bool
type prtabs
val empty_prtabs: prtabs
val update_prtabs: string -> Syntax_Ext.xprod list -> prtabs -> prtabs
@@ -80,6 +82,9 @@
Config.declare "show_question_marks" (fn _ => Config.Bool (! show_question_marks_default));
val show_question_marks = Config.bool show_question_marks_raw;
+fun show_type_constraint ctxt = Config.get ctxt show_types orelse Config.get ctxt show_markup;
+fun show_sort_constraint ctxt = Config.get ctxt show_sorts orelse Config.get ctxt show_markup;
+
(** type prtabs **)