src/Pure/display.ML
changeset 32187 cca43ca13f4f
parent 32145 220c9e439d39
child 32430 de3727f1cf12
equal deleted inserted replaced
32186:8026b73cd357 32187:cca43ca13f4f
    40 structure Display: DISPLAY =
    40 structure Display: DISPLAY =
    41 struct
    41 struct
    42 
    42 
    43 (** options **)
    43 (** options **)
    44 
    44 
    45 val goals_limit = Display_Goal.goals_limit;
    45 val goals_limit = Goal_Display.goals_limit;
    46 val show_consts = Display_Goal.show_consts;
    46 val show_consts = Goal_Display.show_consts;
    47 
    47 
    48 val show_hyps = ref false;      (*false: print meta-hypotheses as dots*)
    48 val show_hyps = ref false;      (*false: print meta-hypotheses as dots*)
    49 val show_tags = ref false;      (*false: suppress tags*)
    49 val show_tags = ref false;      (*false: suppress tags*)
    50 
    50 
    51 
    51 
    85     val hlen = length xshyps + length hyps' + length tpairs;
    85     val hlen = length xshyps + length hyps' + length tpairs;
    86     val hsymbs =
    86     val hsymbs =
    87       if hlen = 0 andalso status = "" then []
    87       if hlen = 0 andalso status = "" then []
    88       else if ! show_hyps orelse show_hyps' then
    88       else if ! show_hyps orelse show_hyps' then
    89         [Pretty.brk 2, Pretty.list "[" "]"
    89         [Pretty.brk 2, Pretty.list "[" "]"
    90           (map (q o Display_Goal.pretty_flexpair ctxt) tpairs @ map prt_term hyps' @
    90           (map (q o Goal_Display.pretty_flexpair ctxt) tpairs @ map prt_term hyps' @
    91            map (Syntax.pretty_sort ctxt) xshyps @
    91            map (Syntax.pretty_sort ctxt) xshyps @
    92             (if status = "" then [] else [Pretty.str status]))]
    92             (if status = "" then [] else [Pretty.str status]))]
    93       else [Pretty.brk 2, Pretty.str ("[" ^ implode (replicate hlen ".") ^ status ^ "]")];
    93       else [Pretty.brk 2, Pretty.str ("[" ^ implode (replicate hlen ".") ^ status ^ "]")];
    94     val tsymbs =
    94     val tsymbs =
    95       if null tags orelse not (! show_tags) then []
    95       if null tags orelse not (! show_tags) then []