src/Pure/General/markup.scala
Mon, 28 Nov 2011 22:05:32 +0100 wenzelm separate module for concrete Isabelle markup;
Fri, 25 Nov 2011 18:37:14 +0100 wenzelm retain stderr and include it in syslog, which is buffered and thus increases the chance that users see remains from crashes etc.;
Thu, 10 Nov 2011 22:32:10 +0100 wenzelm pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
Sun, 04 Sep 2011 19:36:19 +0200 wenzelm eliminated markup for plain identifiers (frequent but insignificant);
Sat, 03 Sep 2011 21:15:35 +0200 wenzelm Document.removed_versions on Scala side;
Fri, 02 Sep 2011 21:48:27 +0200 wenzelm raw message function "assign_execs" avoids full overhead of decoding and caching message body;
Sat, 27 Aug 2011 17:26:14 +0200 wenzelm explicit markup for legacy warnings;
Thu, 25 Aug 2011 16:44:06 +0200 wenzelm propagate information about last command with exec state assignment through document model;
Fri, 19 Aug 2011 14:01:20 +0200 wenzelm Future.promise: explicit abort operation (like uninterruptible future job);
Tue, 12 Jul 2011 19:36:46 +0200 wenzelm more uniform Properties in ML and Scala;
Mon, 11 Jul 2011 16:48:02 +0200 wenzelm JVM method invocation service via Scala layer;
Mon, 11 Jul 2011 11:13:33 +0200 wenzelm some support for raw messages, which bypass standard Symbol/YXML decoding;
Sat, 09 Jul 2011 21:53:27 +0200 wenzelm echo prover input via raw_messages, for improved protocol tracing;
Fri, 08 Jul 2011 17:04:38 +0200 wenzelm discontinued odd Position.column -- left-over from attempts at PGIP implementation;
Tue, 05 Jul 2011 22:39:15 +0200 wenzelm Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;
Wed, 29 Jun 2011 16:31:50 +0200 wenzelm print Path.T with some markup;
Mon, 27 Jun 2011 22:20:49 +0200 wenzelm document antiquotations are managed as theory data, with proper name space and entity markup;
Mon, 27 Jun 2011 16:53:31 +0200 wenzelm ML antiquotations are managed as theory data, with proper name space and entity markup;
Sat, 25 Jun 2011 19:38:35 +0200 wenzelm entity markup for "type", "constant";
Sat, 25 Jun 2011 19:19:13 +0200 wenzelm clarified Markup.CLASS vs. HTML.CLASS;
Sat, 18 Jun 2011 12:37:42 +0200 wenzelm inner literal/delimiter corresponds to outer keyword/operator;
Tue, 14 Jun 2011 14:33:46 +0200 wenzelm more foreground markup, using actual CSS color names;
Wed, 27 Apr 2011 20:28:27 +0200 wenzelm discontinued obsolete markup;
Sun, 17 Apr 2011 20:58:43 +0200 wenzelm markup facts via name space;
Sun, 17 Apr 2011 20:15:46 +0200 wenzelm eliminated obsolete markup -- superseded by generic "entity" markup;
Mon, 11 Apr 2011 17:11:03 +0200 wenzelm Name_Space.entry_markup: keep def position as separate properties;
Sun, 03 Apr 2011 17:35:16 +0200 wenzelm show tooltip/sub-expression for entity markup;
Sun, 27 Mar 2011 21:19:23 +0200 wenzelm added Markup.Name and Markup.Kind convenience;
Sun, 09 Jan 2011 16:03:56 +0100 wenzelm discontinued unused end_line, end_column;
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;
Mon, 04 Jan 2010 18:56:36 +0100 wenzelm explicit markup of document assigment message (simplified variant of earlier "edits" 8c3e1f73953d);
less more (0) -60 tip