src/Pure/General/markup.scala
Wed, 01 Dec 2010 20:34:40 +0100 wenzelm more abstract/uniform handling of time, preferring seconds as Double;
Sat, 06 Nov 2010 18:10:35 +0100 wenzelm somewhat more uniform timing markup in ML vs. Scala;
Sat, 06 Nov 2010 16:53:07 +0100 wenzelm added Markup.Double, Markup.Double_Property;
Wed, 22 Sep 2010 16:04:20 +0200 wenzelm more content for Session_Dockable;
Wed, 22 Sep 2010 13:47:48 +0200 wenzelm main Isabelle_Process via Isabelle_System.Managed_Process;
Sun, 19 Sep 2010 17:12:34 +0200 wenzelm simplified Isabelle_Process message kinds;
Fri, 17 Sep 2010 22:17:57 +0200 wenzelm discontinued Output.debug, which belongs to early PGIP experiments (b6788dbd2ef9) and causes just too many problems (like spamming the message channel if it is used by more than one module);
Fri, 17 Sep 2010 15:51:11 +0200 wenzelm eliminated markup "location" in favour of more explicit "no_report", which is actually deleted from messages;
Tue, 07 Sep 2010 16:08:29 +0200 wenzelm highlight bad range of nested error (here from inner parsing);
Tue, 07 Sep 2010 14:08:21 +0200 wenzelm report token range after inner parse error -- often provides important clues about misunderstanding concerning lexical phase;
Tue, 31 Aug 2010 23:28:21 +0200 wenzelm Command.State: add reported positions to markup tree, according main message position or Markup.binding/entity/report occurrences in body;
Mon, 30 Aug 2010 13:01:32 +0200 wenzelm Command.results: ordered by serial number;
Mon, 30 Aug 2010 11:35:17 +0200 wenzelm message serial number indicates physical order;
Wed, 25 Aug 2010 22:57:40 +0200 wenzelm Pretty: tuned markup objects;
Wed, 25 Aug 2010 22:37:53 +0200 wenzelm organized markup properties via apply/unapply patterns;
Wed, 25 Aug 2010 21:31:22 +0200 wenzelm added some proof state markup, notably number of subgoals (e.g. for indentation);
Wed, 18 Aug 2010 11:02:47 +0200 wenzelm uniform Markup.empty/Markup.Empty in ML and Scala;
Mon, 16 Aug 2010 00:07:28 +0200 wenzelm simplified command status: interpret stacked markup on demand;
Sat, 14 Aug 2010 22:45:23 +0200 wenzelm more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
Wed, 11 Aug 2010 22:41:26 +0200 wenzelm represent document ids by (long) int, to benefit from the somewhat faster Inttab in ML (LinearSet in Scala is invariably indexed by native object ids);
Tue, 10 Aug 2010 12:29:11 +0200 wenzelm distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
Sun, 08 Aug 2010 19:36:31 +0200 wenzelm explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
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 16:00:13 +0200 wenzelm separate markup for ML delimiters;
Sun, 30 May 2010 15:27:49 +0200 wenzelm less pschedelic token markup;
Sat, 29 May 2010 19:46:29 +0200 wenzelm explicit markup for forked goals, as indicated by Goal.fork;
Tue, 25 May 2010 23:03:13 +0200 wenzelm eliminated obsolete priority message from Isabelle_Process protocol;
Thu, 06 May 2010 23:52:20 +0200 wenzelm replaced slightly odd fbreak markup by plain "\n", which also coincides with regular linebreaks produced outside the ML pretty engine;
Thu, 06 May 2010 16:27:47 +0200 wenzelm basic support for symbolic pretty printing;
less more (0) -50 -30 tip