Mon, 28 Nov 2011 22:18:19 +0100 |
wenzelm |
explicit indication of modules for independent Scala library;
|
file |
diff |
annotate
|
Mon, 28 Nov 2011 22:05:32 +0100 |
wenzelm |
separate module for concrete Isabelle markup;
|
file |
diff |
annotate
|
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.;
|
file |
diff |
annotate
|
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;
|
file |
diff |
annotate
|
Sun, 04 Sep 2011 19:36:19 +0200 |
wenzelm |
eliminated markup for plain identifiers (frequent but insignificant);
|
file |
diff |
annotate
|
Sat, 03 Sep 2011 21:15:35 +0200 |
wenzelm |
Document.removed_versions on Scala side;
|
file |
diff |
annotate
|
Fri, 02 Sep 2011 21:48:27 +0200 |
wenzelm |
raw message function "assign_execs" avoids full overhead of decoding and caching message body;
|
file |
diff |
annotate
|
Sat, 27 Aug 2011 17:26:14 +0200 |
wenzelm |
explicit markup for legacy warnings;
|
file |
diff |
annotate
|
Thu, 25 Aug 2011 16:44:06 +0200 |
wenzelm |
propagate information about last command with exec state assignment through document model;
|
file |
diff |
annotate
|
Fri, 19 Aug 2011 14:01:20 +0200 |
wenzelm |
Future.promise: explicit abort operation (like uninterruptible future job);
|
file |
diff |
annotate
|
Tue, 12 Jul 2011 19:36:46 +0200 |
wenzelm |
more uniform Properties in ML and Scala;
|
file |
diff |
annotate
|
Mon, 11 Jul 2011 16:48:02 +0200 |
wenzelm |
JVM method invocation service via Scala layer;
|
file |
diff |
annotate
|
Mon, 11 Jul 2011 11:13:33 +0200 |
wenzelm |
some support for raw messages, which bypass standard Symbol/YXML decoding;
|
file |
diff |
annotate
|
Sat, 09 Jul 2011 21:53:27 +0200 |
wenzelm |
echo prover input via raw_messages, for improved protocol tracing;
|
file |
diff |
annotate
|
Fri, 08 Jul 2011 17:04:38 +0200 |
wenzelm |
discontinued odd Position.column -- left-over from attempts at PGIP implementation;
|
file |
diff |
annotate
|
Tue, 05 Jul 2011 22:39:15 +0200 |
wenzelm |
Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;
|
file |
diff |
annotate
|
Wed, 29 Jun 2011 16:31:50 +0200 |
wenzelm |
print Path.T with some markup;
|
file |
diff |
annotate
|
Mon, 27 Jun 2011 22:20:49 +0200 |
wenzelm |
document antiquotations are managed as theory data, with proper name space and entity markup;
|
file |
diff |
annotate
|
Mon, 27 Jun 2011 16:53:31 +0200 |
wenzelm |
ML antiquotations are managed as theory data, with proper name space and entity markup;
|
file |
diff |
annotate
|
Sat, 25 Jun 2011 19:38:35 +0200 |
wenzelm |
entity markup for "type", "constant";
|
file |
diff |
annotate
|
Sat, 25 Jun 2011 19:19:13 +0200 |
wenzelm |
clarified Markup.CLASS vs. HTML.CLASS;
|
file |
diff |
annotate
|
Sat, 18 Jun 2011 12:37:42 +0200 |
wenzelm |
inner literal/delimiter corresponds to outer keyword/operator;
|
file |
diff |
annotate
|
Tue, 14 Jun 2011 14:33:46 +0200 |
wenzelm |
more foreground markup, using actual CSS color names;
|
file |
diff |
annotate
|
Wed, 27 Apr 2011 20:28:27 +0200 |
wenzelm |
discontinued obsolete markup;
|
file |
diff |
annotate
|
Sun, 17 Apr 2011 20:58:43 +0200 |
wenzelm |
markup facts via name space;
|
file |
diff |
annotate
|
Sun, 17 Apr 2011 20:15:46 +0200 |
wenzelm |
eliminated obsolete markup -- superseded by generic "entity" markup;
|
file |
diff |
annotate
|
Mon, 11 Apr 2011 17:11:03 +0200 |
wenzelm |
Name_Space.entry_markup: keep def position as separate properties;
|
file |
diff |
annotate
|
Sun, 03 Apr 2011 17:35:16 +0200 |
wenzelm |
show tooltip/sub-expression for entity markup;
|
file |
diff |
annotate
|
Sun, 27 Mar 2011 21:19:23 +0200 |
wenzelm |
added Markup.Name and Markup.Kind convenience;
|
file |
diff |
annotate
|
Sun, 09 Jan 2011 16:03:56 +0100 |
wenzelm |
discontinued unused end_line, end_column;
|
file |
diff |
annotate
|
Wed, 01 Dec 2010 20:34:40 +0100 |
wenzelm |
more abstract/uniform handling of time, preferring seconds as Double;
|
file |
diff |
annotate
|
Sat, 06 Nov 2010 18:10:35 +0100 |
wenzelm |
somewhat more uniform timing markup in ML vs. Scala;
|
file |
diff |
annotate
|
Sat, 06 Nov 2010 16:53:07 +0100 |
wenzelm |
added Markup.Double, Markup.Double_Property;
|
file |
diff |
annotate
|
Wed, 22 Sep 2010 16:04:20 +0200 |
wenzelm |
more content for Session_Dockable;
|
file |
diff |
annotate
|
Wed, 22 Sep 2010 13:47:48 +0200 |
wenzelm |
main Isabelle_Process via Isabelle_System.Managed_Process;
|
file |
diff |
annotate
|
Sun, 19 Sep 2010 17:12:34 +0200 |
wenzelm |
simplified Isabelle_Process message kinds;
|
file |
diff |
annotate
|
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);
|
file |
diff |
annotate
|
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;
|
file |
diff |
annotate
|
Tue, 07 Sep 2010 16:08:29 +0200 |
wenzelm |
highlight bad range of nested error (here from inner parsing);
|
file |
diff |
annotate
|
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;
|
file |
diff |
annotate
|
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;
|
file |
diff |
annotate
|
Mon, 30 Aug 2010 13:01:32 +0200 |
wenzelm |
Command.results: ordered by serial number;
|
file |
diff |
annotate
|
Mon, 30 Aug 2010 11:35:17 +0200 |
wenzelm |
message serial number indicates physical order;
|
file |
diff |
annotate
|
Wed, 25 Aug 2010 22:57:40 +0200 |
wenzelm |
Pretty: tuned markup objects;
|
file |
diff |
annotate
|
Wed, 25 Aug 2010 22:37:53 +0200 |
wenzelm |
organized markup properties via apply/unapply patterns;
|
file |
diff |
annotate
|
Wed, 25 Aug 2010 21:31:22 +0200 |
wenzelm |
added some proof state markup, notably number of subgoals (e.g. for indentation);
|
file |
diff |
annotate
|
Wed, 18 Aug 2010 11:02:47 +0200 |
wenzelm |
uniform Markup.empty/Markup.Empty in ML and Scala;
|
file |
diff |
annotate
|
Mon, 16 Aug 2010 00:07:28 +0200 |
wenzelm |
simplified command status: interpret stacked markup on demand;
|
file |
diff |
annotate
|
Sat, 14 Aug 2010 22:45:23 +0200 |
wenzelm |
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
|
file |
diff |
annotate
|
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);
|
file |
diff |
annotate
|
Tue, 10 Aug 2010 12:29:11 +0200 |
wenzelm |
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
|
file |
diff |
annotate
|
Sun, 08 Aug 2010 19:36:31 +0200 |
wenzelm |
explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
|
file |
diff |
annotate
|
Sat, 07 Aug 2010 22:43:57 +0200 |
wenzelm |
simplified some Markup;
|
file |
diff |
annotate
|
Sat, 07 Aug 2010 22:09:52 +0200 |
wenzelm |
simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
|
file |
diff |
annotate
|
Sun, 30 May 2010 16:00:13 +0200 |
wenzelm |
separate markup for ML delimiters;
|
file |
diff |
annotate
|
Sun, 30 May 2010 15:27:49 +0200 |
wenzelm |
less pschedelic token markup;
|
file |
diff |
annotate
|
Sat, 29 May 2010 19:46:29 +0200 |
wenzelm |
explicit markup for forked goals, as indicated by Goal.fork;
|
file |
diff |
annotate
|
Tue, 25 May 2010 23:03:13 +0200 |
wenzelm |
eliminated obsolete priority message from Isabelle_Process protocol;
|
file |
diff |
annotate
|
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;
|
file |
diff |
annotate
|
Thu, 06 May 2010 16:27:47 +0200 |
wenzelm |
basic support for symbolic pretty printing;
|
file |
diff |
annotate
|