src/Pure/Thy/html.scala
Sat, 09 Jan 2016 22:00:22 +0100 wenzelm tuned -- according to ML version;
Fri, 08 Jan 2016 18:18:40 +0100 wenzelm clarified symbol insertion, depending on buffer encoding;
Sun, 03 May 2015 00:01:10 +0200 wenzelm misc tuning, based on warnings by IntelliJ IDEA;
Sun, 12 Apr 2015 13:10:04 +0200 wenzelm less ambitious collection of quasi-generic PIDE modules;
Sat, 29 Nov 2014 14:43:10 +0100 wenzelm encode text with control symbols;
Sat, 26 Apr 2014 14:00:49 +0200 wenzelm clarified PIDE modules;
Sat, 26 Apr 2014 13:32:28 +0200 wenzelm tuned imports;
Thu, 20 Feb 2014 14:36:17 +0100 wenzelm tuned imports;
Sat, 09 Nov 2013 11:41:32 +0100 wenzelm adjust modules for Admin/build jars_test;
Tue, 12 Mar 2013 20:03:04 +0100 wenzelm include session description in chapter index;
Tue, 12 Mar 2013 16:47:24 +0100 wenzelm discontinued "isabelle usedir" option -r (reset session path);
Thu, 03 Jan 2013 20:42:18 +0100 wenzelm maintain session index on Scala side, for more determistic results;
Sun, 25 Nov 2012 19:49:24 +0100 wenzelm Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
Fri, 28 Sep 2012 22:53:18 +0200 wenzelm support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
Thu, 27 Sep 2012 15:55:38 +0200 wenzelm removed obsolete org.w3c.dom operations;
Sat, 10 Mar 2012 23:28:42 +0100 wenzelm discontinued specific entity markup, which causes confusion with "kind" names with spaces (e.g. "type name");
Mon, 28 Nov 2011 22:05:32 +0100 wenzelm separate module for concrete Isabelle markup;
Wed, 17 Aug 2011 16:01:27 +0200 wenzelm some convenience actions/shortcuts for control symbols;
Thu, 07 Jul 2011 13:48:30 +0200 wenzelm simplified Symbol based on lazy Symbol.Interpretation -- reduced odd "functorial style";
Tue, 05 Jul 2011 23:18:14 +0200 wenzelm simplified Symbol.iterator: produce strings, which are mostly preallocated;
Mon, 04 Jul 2011 22:11:32 +0200 wenzelm quasi-static Isabelle_System -- reduced tendency towards "functorial style";
Sat, 25 Jun 2011 18:15:36 +0200 wenzelm type classes: entity markup instead of old-style token markup;
Wed, 22 Jun 2011 20:38:03 +0200 wenzelm clarified decoded control symbols;
Tue, 21 Jun 2011 14:12:49 +0200 wenzelm more uniform treatment of recode_set/recode_map;
Tue, 21 Jun 2011 13:29:44 +0200 wenzelm tuned iteration over short symbols;
Sun, 19 Jun 2011 15:31:16 +0200 wenzelm tuned;
Sun, 19 Jun 2011 15:22:58 +0200 wenzelm discontinued special treatment of \<^loc> (which was original meant as workaround for "local" syntax);
Sun, 19 Jun 2011 14:11:06 +0200 wenzelm some unicode chars for special control symbols;
Sun, 22 Aug 2010 13:52:24 +0200 wenzelm tuned signatures;
Mon, 16 Aug 2010 16:24:22 +0200 wenzelm HTML.spans: explicit flag for preservation of original data (which would be turned into org.w3c.dom user data in XML.document_node);
Sat, 07 Aug 2010 22:43:57 +0200 wenzelm simplified some Markup;
Sat, 07 Aug 2010 22:09:52 +0200 wenzelm simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
Sun, 30 May 2010 23:40:24 +0200 wenzelm added HTML.encode (in Scala), similar to HTML.output in ML;
Tue, 30 Mar 2010 00:47:52 +0200 wenzelm recovered StringBuilder functionality after subtle change of + and ++ in Scala 2.8.0 Beta 1;
Mon, 29 Mar 2010 22:55:57 +0200 wenzelm replaced some deprecated methods;
Mon, 29 Mar 2010 22:43:56 +0200 wenzelm adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;
Sat, 19 Dec 2009 16:51:32 +0100 wenzelm refined some Symbol operations/signatures;
Thu, 10 Dec 2009 13:43:51 +0100 wenzelm sealed XML.Tree;
Mon, 07 Dec 2009 00:02:54 +0100 wenzelm avoid lazy val with side-effects -- spurious null pointers!?
Sun, 06 Dec 2009 23:25:27 +0100 wenzelm proper markup text for loc;
Sun, 06 Dec 2009 23:08:43 +0100 wenzelm basic treatment of special control symbols;
Sun, 06 Dec 2009 22:23:31 +0100 wenzelm more robust treatment of line breaks -- Java "split" has off semantics;
Fri, 04 Dec 2009 22:51:59 +0100 wenzelm Basic HTML output.
less more (0) tip