src/Pure/Thy/html.ML
2010-05-27 wenzelm 2010-05-27 renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;
2009-12-06 wenzelm 2009-12-06 output_syms: permissive treatment of control symbols, cf. Scala version;
2009-12-05 wenzelm 2009-12-05 output linefeed as </br> -- workaround problem with <pre> in Lobo Browser 0.98.4; output_width: uniform mapping -- avoid obscure fastpath optimization;
2009-12-05 wenzelm 2009-12-05 added markup for hidden text; handle "\<^bold>" as markup; HTML output: include original control symbols as hidden text, to enable copy-paste;
2009-12-04 wenzelm 2009-12-04 output "'" as "&#39;" which is a bit more portable ("&apos;" is defined in XML/XHTML, but not in old-style HTML4);
2009-10-27 wenzelm 2009-10-27 critical comments;
2009-09-30 wenzelm 2009-09-30 eliminated dead code;
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-01-21 wenzelm 2009-01-21 removed Ids;
2008-11-18 wenzelm 2008-11-18 tuned;
2008-08-15 wenzelm 2008-08-15 fixed DOCTYPE -- XHTML is case-sensitive!
2008-08-13 wenzelm 2008-08-13 removed obsolete verbatim_source, results, chapter, section etc.; removed redundant end_index, end_theory;
2008-08-11 wenzelm 2008-08-11 <applet>: more XHTML 1.0 Transitional conformance;
2008-08-11 wenzelm 2008-08-11 <pre>: removed xml:space, is already default; result(s): avoid improper nesting of <pre> within <p>;
2008-08-11 wenzelm 2008-08-11 produce XHTML 1.0 Transitional; tuned charset name; renamed Markup.class to Markup.tclass, to avoid potential conflicts with spacial meaning in markup languages (e.g. HTML);
2008-07-08 wenzelm 2008-07-08 removed unused href_opt_name; begin_theory: unconditional file links, proper output of parentheses;
2008-04-17 wenzelm 2008-04-17 replaced token translations by common markup; use XML.text instead of separate escape;
2008-03-28 wenzelm 2008-03-28 Context.>> : operate on Context.generic;
2008-03-27 wenzelm 2008-03-27 eliminated delayed theory setup
2008-03-18 wenzelm 2008-03-18 theory loader: discontinued *attached* ML scripts;
2008-02-21 wenzelm 2008-02-21 more elaborate structure Distribution (filled-in by makedist);
2007-09-15 haftmann 2007-09-15 fixed title
2007-08-13 wenzelm 2007-08-13 Lexicon.read_indexname/nat/variable;
2007-07-31 wenzelm 2007-07-31 with_charset: setmp_noncritical;
2007-07-23 wenzelm 2007-07-23 PrintMode.with_modes;
2007-07-10 wenzelm 2007-07-10 export html_mode, begin_document, end_document;
2007-07-10 wenzelm 2007-07-10 Markup.add_mode;
2007-07-07 wenzelm 2007-07-07 simplified pretty token metric: type int; added command markup; token translations: proper treatment of skolems; separate print_mode setup for Output/Pretty;
2007-04-26 wenzelm 2007-04-26 renamed some old names Theory.xxx to Sign.xxx;
2007-01-19 wenzelm 2007-01-19 results: proper context;
2006-12-15 wenzelm 2006-12-15 avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
2006-09-27 wenzelm 2006-09-27 reverted to 1.58;
2006-09-18 wenzelm 2006-09-18 output: uninterpreted raw symbols -- these are usually LaTeX macros;
2006-07-29 wenzelm 2006-07-29 rename legacy_pretty_thm to pretty_thm_legacy;
2006-07-27 wenzelm 2006-07-27 ProofContext.legacy_pretty_thm;
2006-04-09 wenzelm 2006-04-09 results: smart_pretty_thm uses adhoc proof context if possible;
2006-03-21 wenzelm 2006-03-21 avoid polymorphic equality;
2006-03-14 wenzelm 2006-03-14 Output.add_mode: keyword component;
2006-01-19 wenzelm 2006-01-19 setup: theory -> theory;
2005-09-17 wenzelm 2005-09-17 added with_charset: string -> ('a -> 'b) -> 'a -> 'b;
2005-09-15 wenzelm 2005-09-15 TableFun/Symtab: curried lookup and update;
2005-09-01 wenzelm 2005-09-01 curried_lookup/update;
2005-08-31 wenzelm 2005-08-31 added line break for 'uses';
2005-08-28 wenzelm 2005-08-28 output \<^loc> as 'loc' span; tuned;
2005-08-18 wenzelm 2005-08-18 replace freeze by 'setmp show_question_marks false';
2005-08-16 wenzelm 2005-08-16 begin_index: list of docs;
2005-06-05 wenzelm 2005-06-05 present new-style theory header, with 'imports' and 'uses';
2005-06-02 wenzelm 2005-06-02 html_syms table;
2005-04-21 wenzelm 2005-04-21 superceded by Pure.thy and CPure.thy;
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2004-11-29 kleing 2004-11-29 render \<circ> as o not &circ; (which is ^)
2004-06-22 wenzelm 2004-06-22 tuned output;
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2004-06-20 wenzelm 2004-06-20 Symbol.encode_raw;
2004-05-29 wenzelm 2004-05-29 handle raw symbols; Output.add_mode; more robust handling of sub/superscript;
2004-05-21 wenzelm 2004-05-21 output_tym: removed duplicate clauses;
2004-04-16 berghofe 2004-04-16 Replaced quote by Library.quote, since quote now refers to Symbol.quote
2004-04-15 wenzelm 2004-04-15 fixed width; tuned;
2004-04-14 kleing 2004-04-14 use more symbols in HTML output
2004-04-14 kleing 2004-04-14 prod and sum