module displays. import lj. type display_tactic (goal -> goal -> o) -> o. type text goal -> goal -> o. %type html goal -> goal -> o. %type html_init goal -> goal -> o. type see goal -> goal -> o. display_tactic see. display_tactic text. %display_tactic html. %display_tactic html_init. see In In :- term_to_string In Str, print "Internal form of sequent:\n", print Str, print "\n". text In In :- write_seq In. %html G G :- html_seq G. % %html_init G G :- % html_open_out "seq.html" (ooo % "\ % \Display of sequents\n\ % \\n\n" % ).