jHOLLight/JHOL.app/Contents/Resources/Java/newprinter.ml

   1 include Format;;
   2
   3 set_max_boxes 100;;
   4
   5
   6 (* ------------------------------------------------------------------------- *)
   7 (* Protection for HTML output                                                *)
   8 (* ------------------------------------------------------------------------- *)
   9  let output_functions = get_all_formatter_output_functions();;
  10 let make n s=
  11   let rec make_aux n s str =
  12     match n with
  13     | 0 -> str
  14     | _ -> make_aux (n - 1) s (str ^ s)
  15   in
  16   make_aux n s "";;
  17
  18 let new_output_functions (x,y,z,w) = set_all_formatter_output_functions x y  (fun () ->x "<br>" 0 4) (fun n -> x (make n "&#160;")  0 (6 * n));;
  19  let restore_output_functions (x,y,z,w) = set_all_formatter_output_functions x y z w;;
  20
  21 let pp_print_string' = pp_print_string;;
  22 let print_string' = print_string;;
  23 let rec pp_print_string fmt str =
  24 match (String.length str) with
  25 | 0 -> ()
  26 |_->
  27 if (Str.string_match (Str.regexp "!") str 0)
  28 then begin
  29 pp_print_as fmt 1 "&#8704;";
  30 pp_print_string fmt (String.sub str 1 ((String.length str) - 1))
  31 end
  32 else
  33 if (Str.string_match (Str.regexp "\?") str 0)
  34 then begin
  35 pp_print_as fmt 1 "&#8707;";
  36 pp_print_string fmt (String.sub str 1 ((String.length str) - 1))
  37 end
  38 else
  39 if (Str.string_match (Str.regexp "--") str 0)
  40 then begin
  41 pp_print_as fmt 1 "&#8722;";
  42 pp_print_string fmt (String.sub str 2 ((String.length str) - 2))
  43 end
  44 else
  45 if (Str.string_match (Str.regexp "|-") str 0)
  46 then begin
  47 pp_print_as fmt 1 "&#8866;";
  48 pp_print_string fmt (String.sub str 2 ((String.length str) - 2))
  49 end
  50 else
  51 if (Str.string_match (Str.regexp "~") str 0)
  52 then begin
  53 pp_print_as fmt 1 "&#172;";
  54 pp_print_string fmt (String.sub str 1 ((String.length str) - 1))
  55 end
  56 else
  57 if (Str.string_match (Str.regexp "<=>") str 0)
  58 then begin
  59 pp_print_as fmt 1 "&#8660;";
  60 pp_print_string fmt (String.sub str 3 ((String.length str) - 3))
  61 end
  62 else
  63 if (Str.string_match (Str.regexp "==>") str 0)
  64 then begin
  65 pp_print_as fmt 1 "&#8658;";
  66 pp_print_string fmt (String.sub str 3 ((String.length str) - 3))
  67 end
  68 else
  69 if (Str.string_match (Str.regexp ">=") str 0)
  70 then begin
  71 pp_print_as fmt 1 "&#8805;";
  72 pp_print_string fmt (String.sub str 2 ((String.length str) - 2))
  73 end
  74 else
  75 if (Str.string_match (Str.regexp "<=") str 0)
  76 then begin
  77 pp_print_as fmt 1 "&#8804;";
  78 pp_print_string fmt (String.sub str 2 ((String.length str) - 2))
  79 end
  80 else
  81 if (Str.string_match (Str.regexp "\\\\/") str 0)
  82 then begin
  83 pp_print_as fmt 1 "&#8744;";
  84 pp_print_string fmt (String.sub str 2 ((String.length str) - 2))
  85 end
  86 else
  87 if (Str.string_match (Str.regexp "/\\\\") str 0)
  88 then begin
  89 pp_print_as fmt 1 "&#8743;";
  90 pp_print_string fmt (String.sub str 2 ((String.length str) - 2))
  91 end
  92 else
  93 if (Str.string_match (Str.regexp "\\\\") str 0)
  94 then begin
  95 pp_print_as fmt 1 "&#955;";
  96 pp_print_string fmt (String.sub str 1 ((String.length str) - 1))
  97 end
  98 else
  99 if (Str.string_match (Str.regexp ">") str 0)
 100 then begin
 101 pp_print_as fmt 1 "&#62;";
 102 pp_print_string fmt (String.sub str 1 ((String.length str) - 1))
 103 end
 104 else
 105 if (Str.string_match (Str.regexp "<") str 0)
 106 then begin
 107 pp_print_as fmt 1 "&#60;";
 108 pp_print_string fmt (String.sub str 1 ((String.length str) - 1))
 109 end
 110 else
 111 if (Str.string_match (Str.regexp " ") str 0)
 112 then begin
 113 pp_print_as fmt 1 "&#160;";
 114 pp_print_string fmt (String.sub str 1 ((String.length str) - 1))
 115 end
 116 else
 117 begin
 118 pp_print_as fmt 1 (String.sub str 0 1);
 119 pp_print_string fmt  (String.sub str 1 ((String.length str) - 1))
 120 end;;
 121 let print_string = pp_print_string std_formatter;;
 122
 123 (* ------------------------------------------------------------------------- *)
 124 (* Determine binary operators that print without surrounding spaces.         *)
 125 (* ------------------------------------------------------------------------- *)
 126
 127 let unspaced_binops = ref [","; ".."; "$"];;
 128
 129 (* ------------------------------------------------------------------------- *)
 130 (* Binary operators to print at start of line when breaking.                 *)
 131 (* ------------------------------------------------------------------------- *)
 132
 133 let prebroken_binops = ref ["==>"];;
 134
 135 (* ------------------------------------------------------------------------- *)
 136 (* Force explicit indications of bound variables in set abstractions.        *)
 137 (* ------------------------------------------------------------------------- *)
 138
 139 (* let print_unambiguous_comprehensions = ref false;; *)
 140
 141    (* ------------------------------------------------------------------------- *)
 142    (* Print the universal set UNIV:A->bool as "(:A)".                           *)
 143    (* ------------------------------------------------------------------------- *)
 144
 145    let typify_universal_set = ref true;;
 146
 147    (* ------------------------------------------------------------------------- *)
 148    (* Flag controlling whether hypotheses print.                                *)
 149    (* ------------------------------------------------------------------------- *)
 150
 151    let print_all_thm = ref true;;
 152
 153    (* ------------------------------------------------------------------------- *)
 154    (* Flag determining whether interface/overloading is reversed on printing.   *)
 155    (* ------------------------------------------------------------------------- *)
 156    let reverse_interface_mapping = ref true;;
 157
 158    (* ------------------------------------------------------------------------- *)
 159    (* Uses the_interface to lookup the names of operators                       *)
 160    (* ------------------------------------------------------------------------- *)
 161    let reverse_interface (s0,ty0) =
 162    if not(!reverse_interface_mapping) then s0 else
 163    try fst(find (fun (s,(s',ty)) -> s' = s0 & can (type_match ty ty0) [])
 164                 (!the_interface))
 165    with Failure _ -> s0;;
 166
 167    (* ------------------------------------------------------------------------- *)
 168    (* Get the name of a constant or variable.                                   *)
 169    (* ------------------------------------------------------------------------- *)
 170
 171    let name_of tm =
 172    match tm with
 173    Var(x,ty) | Const(x,ty) -> x
 174   | _ -> "";;
 175
 176   (* ------------------------------------------------------------------------- *)
 177   (* Printer for types.                                                        *)
 178   (* ------------------------------------------------------------------------- *)
 179
 180   let pp_print_type,pp_print_qtype =
 181   let soc sep flag ss =
 182   if ss = [] then "" else
 183   let s = end_itlist (fun s1 s2 -> s1^sep^s2) ss in
 184   if flag then "("^s^")" else s in
 185   let rec sot pr ty =
 186   try dest_vartype ty with Failure _ ->
 187   match dest_type ty with
 188   con,[] -> con
 189   | "fun",[ty1;ty2] -> soc "->" (pr > 0) [sot 1 ty1; sot 0 ty2]
 190     | "sum",[ty1;ty2] -> soc "+" (pr > 2) [sot 3 ty1; sot 2 ty2]
 191     | "prod",[ty1;ty2] -> soc "#" (pr > 4) [sot 5 ty1; sot 4 ty2]
 192     | "cart",[ty1;ty2] -> soc "^" (pr > 6) [sot 6 ty1; sot 7 ty2]
 193     | con,args -> (soc "," true (map (sot 0) args))^con in
 194   (fun fmt ty -> pp_print_string fmt (sot 0 ty)),
 195   (fun fmt ty -> pp_print_string fmt ("`:" ^ sot 0 ty ^ "`"));;
 196
 197 (* ------------------------------------------------------------------------- *)
 198 (* This returns L and R  if OP = c  in  (tm:= L OP R)                        *)
 199 (* ------------------------------------------------------------------------- *)
 200 let dest_binary' c tm =
 201 try let il,r = dest_comb tm in
 202 let i,l = dest_comb il in
 203 if i = c or
 204 (is_const i & is_const c &
 205           reverse_interface(dest_const i) = reverse_interface(dest_const c))
 206 then l,r else fail()
 207 with Failure _ -> failwith "dest_binary";;
 208
 209 (* ------------------------------------------------------------------------- *)
 210 (* string -> bool   Lookup to see if operator of string is right assoc       *)
 211 (* ------------------------------------------------------------------------- *)
 212 let is_right_assoc s =
 213 match snd(get_infix_status s) with
 214 |"right" -> true
 215       | _ -> false;;
 216
 217 (* ------------------------------------------------------------------------- *)
 218 (* num -> bool                                                               *)
 219 (* ------------------------------------------------------------------------- *)
 220 let rec power_of_10 n =
 221 if abs_num n </ Int 1 then false
 222 else if n =/ Int 1 then true
 223 else power_of_10 (n // Int 10);;
 224
 225 (* ------------------------------------------------------------------------- *)
 226 (* term -> bool           converts bool term to ocaml bool                   *)
 227 (* ------------------------------------------------------------------------- *)
 228 let bool_of_term t =
 229 match t with
 230 Const("T",_) -> true
 231 | Const("F",_) -> false
 232     | _ -> failwith "bool_of_term";;
 233
 234 (* ------------------------------------------------------------------------- *)
 235 (* term -> int            converts ASCII term into int equiv                 *)
 236 (* ------------------------------------------------------------------------- *)
 237 let code_of_term t =
 238 let f,tms = strip_comb t in
 239 if not(is_const f & fst(dest_const f) = "ASCII")
 240 or not(length tms = 8) then failwith "code_of_term"
 241 else
 242 itlist (fun b f -> if b then 1 + 2 * f else 2 * f)
 243 (map bool_of_term (rev tms)) 0;;
 244
 245 (* ------------------------------------------------------------------------- *)
 246 (*                       *)
 247 (* ------------------------------------------------------------------------- *)
 248 let rec dest_clause tm =
 249 let pbod = snd(strip_exists(body(body tm))) in
 250 let s,args = strip_comb pbod in
 251 if name_of s = "_UNGUARDED_PATTERN" & length args = 2 then
 252 [rand(rator(hd args));rand(rator(hd(tl args)))]
 253 else if name_of s = "_GUARDED_PATTERN" & length args = 3 then
 254 [rand(rator(hd args)); hd(tl args); rand(rator(hd(tl(tl args))))]
 255 else failwith "dest_clause" ;;
 256
 257 (* ------------------------------------------------------------------------- *)
 258 (*                         *)
 259 (* ------------------------------------------------------------------------- *)
 260 let rec dest_clauses tm =
 261 let s,args = strip_comb tm in
 262 if name_of s = "_SEQPATTERN" & length args = 2 then
 263 dest_clause (hd args)::dest_clauses(hd(tl args))
 264 else [dest_clause tm];;
 265
 266
 267 (* ------------------------------------------------------------------------- *)
 268 (* Allow the installation of user printers. Must fail quickly if N/A.        *)
 269 (* ------------------------------------------------------------------------- *)
 270 let install_user_printer,delete_user_printer,try_user_printer =
 271 let user_printers = ref ([]:(string*(term->unit))list) in
 272 (fun pr -> user_printers := pr::(!user_printers)),
 273 (fun s -> user_printers := snd(remove (fun (s',_) -> s = s')
 274                                       (!user_printers))),
 275 (fun tm -> tryfind (fun (_,pr) -> pr tm) (!user_printers));;
 276
 277
 278
 279
 280
 281 (* ------------------------------------------------------------------------- *)
 282 (* Type to determine how/(what tag) to print                                 *)
 283 (* ------------------------------------------------------------------------- *)
 284 type term_type = Numeral | List | Char_list | Generalized_abstraction |
 285 Empty | Universal | G_spec | Let | Decimal | Match | Function |
 286           Insert | Cond | Other;;
 287
 288 (* ------------------------------------------------------------------------- *)
 289 (* term -> term_type                                                         *)
 290 (* ------------------------------------------------------------------------- *)
 291 let rec get_term_type tm =
 292 if is_numeral tm then Numeral
 293 else if is_list tm then
 294 begin
 295 try if fst(dest_type(hd(snd(dest_type(type_of tm))))) <> "char"
 296 then fail()
 297 else Char_list with Failure _ -> List
 298 end
 299 else if is_gabs tm then Generalized_abstraction
 300 else
 301 begin
 302 let hop,args = strip_comb tm in
 303 let s0 = name_of hop
 304 and ty0 = type_of hop in
 305 let s = reverse_interface (s0,ty0) in
 306 if s = "EMPTY" & is_const tm & args = [] then Empty
 307 else if s = "UNIV" & !typify_universal_set & is_const tm & args = []
 308 then Universal
 309 else if s = "INSERT" &
 310 is_const (snd(splitlist (dest_binary "INSERT") tm))  &
 311 fst(
 312     dest_const (
 313                 snd(
 314                     splitlist (
 315                                dest_binary "INSERT") tm))) = "EMPTY" then Insert
 316 else if (s = "GSPEC") &
 317 fst(dest_const (
 318                 (rator o
 319                        fst o dest_comb o
 320                        fst o dest_comb o
 321                        snd o strip_exists
 322                        o body o rand)tm )) = "SETSPEC" then G_spec
 323 else if is_let tm then Let
 324 else if s = "DECIMAL" &
 325 (power_of_10 ((dest_numeral o hd o tl)args)) then Decimal
 326 else if s = "_MATCH" &
 327 length args = 2 then Match
 328 else if s = "_FUNCTION" &
 329 length args = 1 then Function
 330 else if s = "COND" & length args = 3 then Cond
 331 else Other
 332 end;;
 333
 334
 335 (* ------------------------------------------------------------------------- *)
 336 (* Printer for terms.                                                        *)
 337 (* ------------------------------------------------------------------------- *)
 338 let pp_print_term =
 339 fun fmt ->
 340 let rec print_subterm prec tm =
 341 try try_user_printer tm with Failure _ ->
 342 let hop,args = strip_comb tm in
 343 let s0 = name_of hop
 344 and ty0 = type_of hop in
 345 let s = reverse_interface (s0,ty0) in
 346 match get_term_type tm with
 347 | Numeral ->
 348                   begin
 349                     open_tag "span class=\"Numeral\"";
 350                     pp_print_string fmt (string_of_num(dest_numeral tm));
 351                     close_tag();
 352                   end;
 353               |Char_list ->
 354 begin
 355 open_tag "span class=\"Char_list\"";
 356 pp_print_string fmt (
 357                      "\"" ^ String.escaped (implode (map (
 358                                                           String.make 1 o
 359                                                                       Char.chr o
 360                                                                       code_of_term )
 361                                                          (dest_list tm) )) ^ "\"");
 362 close_tag();
 363 end;
 364 |List ->
 365                  begin
 366                    open_tag "span class=\"List\"";
 367                    pp_print_string fmt "[";
 368                    print_term_sequence "; " 0 (dest_list tm);
 369                    pp_print_string fmt "]";
 370                    close_tag();
 371                  end;
 372               |Generalized_abstraction ->
 373 begin
 374 open_tag "span class=\"Generalized_abstraction\"";
 375 print_binder prec tm;
 376 close_tag();
 377 end
 378 |Empty ->
 379                  begin
 380                    open_tag "span class=\"Empty\"";
 381                    pp_print_string fmt "{}";
 382                    close_tag();
 383                  end
 384               |Universal ->
 385 begin
 386 let ty = fst(dest_fun_ty(type_of tm)) in
 387 begin
 388 open_tag "span class=\"Universal\"";
 389 pp_print_string fmt "(:";
 390 pp_print_type fmt ty;
 391 pp_print_string fmt ")";
 392 close_tag();
 393 end
 394 end;
 395 |Insert ->
 396                  begin
 397                    open_tag "span class=\"Insert\"";
 398                    pp_print_string fmt "{";
 399                    print_term_sequence ", " 14 (
 400                      fst(
 401                        splitlist (dest_binary "INSERT") tm));
 402                    pp_print_string fmt "}";
 403                    close_tag();
 404                  end;
 405               |G_spec ->
 406 begin
 407
 408 let evs,bod = strip_exists(body(rand tm)) in
 409 let bod1,fabs = dest_comb bod in
 410 let bod2,babs = dest_comb bod1 in
 411 (* let c = rator bod2 in*)
 412
 413 (* (let fvs = frees fabs and bvs = frees babs in
 414         if not(!print_unambiguous_comprehensions) &
 415         set_eq evs
 416         (if (length fvs <= 1 or bvs = []) then fvs
 417             else intersect fvs bvs)
 418         then ()
 419         else (print_term_sequence "," 14 evs;
 420                                   pp_print_string fmt " | "));
 421    *)
 422 open_tag "span class=\"G_spec\"";
 423 pp_print_string fmt "{";
 424 print_subterm 0 fabs;
 425 pp_print_string fmt " | ";
 426 print_subterm 0 babs;
 427 pp_print_string fmt "}";
 428 close_tag();
 429 end;
 430 |Let ->
 431                  begin
 432                    open_tag "span class=\"Let\"";
 433                    let eqs,bod = dest_let tm in
 434                      (if prec = 0 then pp_open_hvbox fmt 0
 435                       else (pp_open_hvbox fmt 1; pp_print_string fmt "(");
 436                       pp_print_string fmt "let ";
 437                       print_subterm 0 (mk_eq(hd eqs));
 438                       do_list (fun (v,t) -> pp_print_break fmt 1 0;
 439                                  pp_print_string fmt "and ";
 440                                  print_subterm 0 (mk_eq(v,t)))
 441                         (tl eqs);
 442                       pp_print_string fmt " in";
 443                       pp_print_break fmt 1 0;
 444                       print_subterm 0 bod;
 445                       if prec = 0 then () else pp_print_string fmt ")";
 446                       pp_close_box fmt ());
 447                      close_tag();
 448                  end;
 449               |Decimal ->
 450 begin
 451 open_tag "span class=\"Decimal\"";
 452 let n_num = dest_numeral (hd args)
 453 and n_den = dest_numeral (hd(tl args)) in
 454 let s_num = string_of_num(quo_num n_num n_den) in
 455 let s_den = implode(
 456                     tl(explode(string_of_num
 457                                (n_den +/ (mod_num n_num n_den))))) in
 458 pp_print_string fmt(
 459                     "#"^s_num^(if n_den = Int 1 then "" else ".")^s_den);
 460 close_tag();
 461 end;
 462 |Match ->
 463                  begin
 464
 465                    open_tag "span class=\"Match\"";
 466                    let cls = dest_clauses(hd(tl args)) in
 467                      (if prec = 0 then () else pp_print_string fmt "(";
 468                       pp_open_hvbox fmt 0;
 469                       pp_print_string fmt "match ";
 470                       print_subterm 0 (hd args);
 471                       pp_print_string fmt " with";
 472                       pp_print_break fmt 1 2;
 473                       print_clauses cls;
 474                       pp_close_box fmt ();
 475                       if prec = 0 then () else pp_print_string fmt ")");
 476                      close_tag();
 477                  end
 478               |Function ->
 479 begin
 480 open_tag "span class=\"Function\"";
 481 let cls = dest_clauses(hd args) in
 482 (if prec = 0 then () else pp_print_string fmt "(";
 483     pp_open_hvbox fmt 0;
 484     pp_print_string fmt "function";
 485     pp_print_break fmt 1 2;
 486     print_clauses cls;
 487     pp_close_box fmt ();
 488     if prec = 0 then () else pp_print_string fmt ")");
 489 close_tag();
 490 end
 491 |Cond ->
 492                  begin
 493                    open_tag "span class=\"Cond\"";
 494
 495                    (if prec = 0 then () else pp_print_string fmt "(";
 496                     pp_open_hvbox fmt (-1);
 497                     pp_print_string fmt "if ";
 498                     print_subterm 0 (hd args);
 499                     pp_print_break fmt 0 0;
 500                     pp_print_string fmt " then ";
 501                     print_subterm 0 (hd(tl args));
 502                     pp_print_break fmt 0 0;
 503                     pp_print_string fmt " else ";
 504                     print_subterm 0 (hd(tl(tl args)));
 505                     pp_close_box fmt ();
 506                     if prec = 0 then () else pp_print_string fmt ")");
 507                    close_tag();
 508                  end
 509               |_ ->
 510 begin
 511 if is_prefix s & length args = 1 then
 512 (if prec = 1000 then pp_print_string fmt "(" else ();
 513     pp_print_string fmt s;
 514     (if isalnum s or
 515         s = "--" &
 516         length args = 1 &
 517         (try let l,r = dest_comb(hd args) in
 518              let s0 = name_of l in
 519              s0 = "--" or
 520              mem (fst(dest_const l)) ["real_of_num"; "int_of_num"]
 521              with Failure _ -> false) or
 522              s = "~" & length args = 1 & is_neg(hd args)
 523              then pp_print_string fmt " " else ());
 524     print_subterm 999 (hd args);
 525     if prec = 1000 then pp_print_string fmt ")" else ())
 526 else if parses_as_binder s & length args = 1 & is_gabs (hd args) then
 527 print_binder prec tm
 528 else if can get_infix_status s & length args = 2 then
 529 let bargs =
 530 if is_right_assoc s then
 531 let tms,tmt = splitlist (dest_binary' hop) tm in tms@[tmt]
 532 else
 533 let tmt,tms = rev_splitlist (dest_binary' hop) tm in tmt::tms in
 534 let newprec = fst(get_infix_status s) in
 535 (if newprec <= prec then
 536     (pp_open_hvbox fmt 1; pp_print_string fmt "(")
 537                    else pp_open_hvbox fmt 0;
 538                    print_subterm newprec (hd bargs);
 539                    do_list (fun x -> if mem s (!unspaced_binops) then ()
 540                                 else if mem s (!prebroken_binops)
 541                                 then pp_print_break fmt 1 0
 542                                 else pp_print_string fmt " ";
 543                                 pp_print_string fmt s;
 544                                 if mem s (!unspaced_binops)
 545                                 then pp_print_break fmt 0 0
 546                                 else if mem s (!prebroken_binops)
 547                                 then pp_print_string fmt " "
 548                                 else pp_print_break fmt 1 0;
 549                                 print_subterm newprec x) (tl bargs);
 550                                 if newprec <= prec then pp_print_string fmt ")" else ();
 551                                 pp_close_box fmt ())
 552     else if (is_const hop or is_var hop) & args = [] then
 553     let s' = if parses_as_binder s or can get_infix_status s or is_prefix s
 554     then "("^s^")" else s in
 555     pp_print_string fmt s'
 556     else
 557     let l,r = dest_comb tm in
 558     (pp_open_hvbox fmt 0;
 559                    if prec = 1000 then pp_print_string fmt "(" else ();
 560                    print_subterm 999 l;
 561                    (if try mem (fst(dest_const l)) ["real_of_num"; "int_of_num"]
 562                        with Failure _ -> false
 563                        then () else pp_print_space fmt ());
 564                    print_subterm 1000 r;
 565                    if prec = 1000 then pp_print_string fmt ")" else ();
 566                    pp_close_box fmt ())
 567
 568     end
 569
 570
 571
 572     (* Code is safe down here *)
 573
 574
 575
 576
 577     and   print_term_sequence sep prec tms =
 578     if tms = [] then () else
 579     (print_subterm prec (hd tms);
 580                    let ttms = tl tms in
 581                    if ttms = [] then ()
 582                    else (pp_print_string fmt sep; print_term_sequence sep prec ttms))
 583
 584
 585                                          and   print_clauses cls =
 586                                          match cls with
 587                                          [c] -> print_clause c
 588                                          | c::cs -> (print_clause c;
 589                       pp_print_break fmt 1 0;
 590                       pp_print_string fmt "| ";
 591                       print_clauses cs)
 592
 593       and   print_binder prec tm =
 594         let absf = is_gabs tm in
 595         let s = if absf then "\\" else name_of(rator tm) in
 596         let rec collectvs tm =
 597                    if absf then
 598                      if is_abs tm then
 599                        let v,t = dest_abs tm in
 600                        let vs,bod = collectvs t in (false,v)::vs,bod
 601                      else if is_gabs tm then
 602                        let v,t = dest_gabs tm in
 603                        let vs,bod = collectvs t in (true,v)::vs,bod
 604                      else [],tm
 605                    else if is_comb tm & name_of(rator tm) = s then
 606                      if is_abs(rand tm) then
 607                        let v,t = dest_abs(rand tm) in
 608                        let vs,bod = collectvs t in (false,v)::vs,bod
 609                      else if is_gabs(rand tm) then
 610                        let v,t = dest_gabs(rand tm) in
 611                        let vs,bod = collectvs t in (true,v)::vs,bod
 612                      else [],tm
 613                    else [],tm in
 614         let vs,bod = collectvs tm in
 615           begin
 616             open_tag "span class=\"binder\"";
 617             (if prec = 0 then pp_open_hvbox fmt 4
 618             else (pp_open_hvbox fmt 5; pp_print_string fmt "("));
 619            pp_print_string fmt s;
 620            (if isalnum s then pp_print_string fmt " " else ());
 621            do_list (fun (b,x) ->
 622                       (if b then pp_print_string fmt "(" else ());
 623                       print_subterm 0 x;
 624                       (if b then pp_print_string fmt ")" else ());
 625                       pp_print_string fmt " ") (butlast vs);
 626            (if fst(last vs) then pp_print_string fmt "(" else ());
 627            print_subterm 0 (snd(last vs));
 628            (if fst(last vs) then pp_print_string fmt ")" else ());
 629            pp_print_string fmt ".";
 630            (if length vs = 1 then pp_print_string fmt " "
 631             else pp_print_space fmt ());
 632            print_subterm 0 bod;
 633            (if prec = 0 then () else pp_print_string fmt ")");
 634            pp_close_box fmt ();
 635            close_tag();
 636           end;
 637
 638       and print_clause cl =
 639         match cl with
 640             [p;g;r] -> (print_subterm 1 p;
 641                         pp_print_string fmt " when ";
 642                         print_subterm 1 g;
 643                         pp_print_string fmt " -> ";
 644                         print_subterm 1 r)
 645                    | [p;r] -> (print_subterm 1 p;
 646                                pp_print_string fmt " -> ";
 647                                print_subterm 1 r)
 648       in print_subterm 0;;
 649
 650 (* ------------------------------------------------------------------------- *)
 651 (* Print term with quotes.                                                   *)
 652 (* ------------------------------------------------------------------------- *)
 653
 654 let pp_print_qterm fmt tm =
 655 new_output_functions output_functions;
 656 open_tag "HTML";
 657 open_tag "HEAD";
 658 open_tag "TITLE";
 659 close_tag ();
 660 open_tag "style type=\"text/css\"";
 661 pp_print_as fmt 0 ".real {color:teal; background-color:white; font-weight:bold; text-align:center;} .num {color:fuchsia; background-color:white; font-weight:bold; text-align:center;} .int {color:olive; background-color:white; font-weight:bold; text-align:center;}";
 662 close_tag();
 663 close_tag();
 664 open_tag "BODY";
 665 open_tag "TT";
 666 pp_print_term fmt tm;
 667 close_tag();
 668 close_tag();
 669 close_tag();
 670 restore_output_functions output_functions;;
 671
 672
 673 (* ------------------------------------------------------------------------- *)
 674 (* Printer for theorems.                                                     *)
 675 (* ------------------------------------------------------------------------- *)
 676
 677 let pp_print_thm fmt th =
 678 let asl,tm = dest_thm th in
 679 (if not (asl = []) then
 680     (if !print_all_thm then
 681       (pp_print_term fmt (hd asl);
 682                      do_list (fun x -> pp_print_string fmt ",";
 683                                   pp_print_space fmt ();
 684                                   pp_print_term fmt x)
 685                      (tl asl))
 686       else pp_print_string fmt "...";
 687       pp_print_space fmt ())
 688     else ();
 689     pp_open_hbox fmt();
 690
 691     pp_print_string fmt "|- ";
 692     pp_print_term fmt tm;
 693     pp_close_box fmt ());;
 694
 695 let pp_print_thm' = pp_print_thm;;
 696 let pp_print_thm fmt tm =
 697 new_output_functions output_functions;
 698 open_tag "HTML";
 699 open_tag "HEAD";
 700 open_tag "TITLE";
 701 close_tag();
 702 open_tag "style type=\"text/css\"";
 703 pp_print_as fmt 0 ".real {color:teal; background-color:white; font-weight:bold; text-align:center;} .num {color:fuchsia; background-color:white; font-weight:bold; text-align:center;} .int {color:olive; background-color:white; font-weight:bold; text-align:center;}";
 704 close_tag();
 705 close_tag();
 706 open_tag "BODY";
 707 open_tag "TT";
 708 pp_print_thm fmt tm;
 709 close_tag();
 710 close_tag();
 711 close_tag();
 712 restore_output_functions output_functions;;
 713
 714
 715 (* ------------------------------------------------------------------------- *)
 716 (* Print on standard output.                                                 *)
 717 (* ------------------------------------------------------------------------- *)
 718
 719 let print_type = pp_print_type std_formatter;;
 720 let print_qtype = pp_print_qtype std_formatter;;
 721 let print_term = pp_print_term std_formatter;;
 722 let print_qterm = pp_print_qterm std_formatter;;
 723 let print_thm = pp_print_thm std_formatter;;
 724
 725 (* ------------------------------------------------------------------------- *)
 726 (* Install all the printers.                                                 *)
 727 (* ------------------------------------------------------------------------- *)
 728
 729 #install_printer print_qtype;;
 730 #install_printer print_qterm;;
 731 #install_printer print_thm;;
 732
 733 (* ------------------------------------------------------------------------- *)
 734 (* Conversions to string.                                                    *)
 735 (* ------------------------------------------------------------------------- *)
 736
 737 let print_to_string printer =
 738 let sbuff = ref "" in
 739 let output s m n = sbuff := (!sbuff)^(String.sub s m n) and flush() = () in
 740 let fmt = make_formatter output flush in
 741 ignore(pp_set_max_boxes fmt 100);
 742 fun i -> ignore(printer fmt i);
 743 ignore(pp_print_flush fmt ());
 744 let s = !sbuff in sbuff := ""; s;;
 745
 746 let string_of_type = print_to_string pp_print_type;;
 747 let string_of_term = print_to_string pp_print_term;;
 748 let string_of_thm = print_to_string pp_print_thm;;
 749
 750 (* ------------------------------------------------------------------------- *)
 751 (* Print types                                                               *)
 752 (* ------------------------------------------------------------------------- *)
 753
 754 let print_typed_var tm =
 755 let s,ty = dest_var tm in
 756 begin
 757 open_tag("span class=\""^(string_of_type ty)^"\"");
 758 print_string(s);
 759 close_tag();
 760 end in
 761 install_user_printer("print_typed_var", print_typed_var);;
 762 set_mark_tags true;;
 763
 764 let pp_print_string = pp_print_string';;
 765 let print_string = print_string';;
 766
 767
 768