Sat, 13 Aug 2011 20:20:36 +0200 |
wenzelm |
provide node header via Scala layer;
|
file |
diff |
annotate
|
Sat, 13 Aug 2011 15:59:26 +0200 |
wenzelm |
clarified node header -- exclude master_dir;
|
file |
diff |
annotate
|
Fri, 12 Aug 2011 12:03:17 +0200 |
wenzelm |
simplified class Thy_Header;
|
file |
diff |
annotate
|
Fri, 12 Aug 2011 11:41:26 +0200 |
wenzelm |
clarified Exn.message;
|
file |
diff |
annotate
|
Thu, 11 Aug 2011 20:32:44 +0200 |
wenzelm |
uniform treatment of header edits as document edits;
|
file |
diff |
annotate
|
Thu, 11 Aug 2011 18:01:28 +0200 |
wenzelm |
explicit datatypes for document node edits;
|
file |
diff |
annotate
|
Tue, 12 Jul 2011 10:44:30 +0200 |
wenzelm |
tuned XML modules;
|
file |
diff |
annotate
|
Mon, 11 Jul 2011 16:48:02 +0200 |
wenzelm |
JVM method invocation service via Scala layer;
|
file |
diff |
annotate
|
Sun, 10 Jul 2011 20:59:04 +0200 |
wenzelm |
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
|
file |
diff |
annotate
|
Sun, 10 Jul 2011 13:51:21 +0200 |
wenzelm |
simplified XML_Data;
|
file |
diff |
annotate
|
Sun, 10 Jul 2011 13:00:22 +0200 |
wenzelm |
less currying in Scala;
|
file |
diff |
annotate
|
Sun, 10 Jul 2011 00:21:19 +0200 |
wenzelm |
propagate header changes to prover process;
|
file |
diff |
annotate
|
Thu, 11 Nov 2010 17:07:05 +0100 |
wenzelm |
unified type Document.Edit;
|
file |
diff |
annotate
|
Thu, 23 Sep 2010 15:36:03 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Thu, 23 Sep 2010 14:39:29 +0200 |
wenzelm |
tuned prover message categorization;
|
file |
diff |
annotate
|
Wed, 22 Sep 2010 22:39:17 +0200 |
wenzelm |
Command.accumulate: refrain from adding tracing messages to markup tree -- potential scalability problem;
|
file |
diff |
annotate
|
Fri, 17 Sep 2010 21:49:34 +0200 |
wenzelm |
some specific message classification;
|
file |
diff |
annotate
|
Fri, 17 Sep 2010 17:10:44 +0200 |
wenzelm |
allow embedded reports in regular prover messages, to avoid side-effects for errors for example;
|
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 23:59:14 +0200 |
wenzelm |
Document_View: select gutter message icons from markup over line range, not full range results;
|
file |
diff |
annotate
|
Tue, 07 Sep 2010 18:44:28 +0200 |
wenzelm |
basic support for warning/error gutter icons;
|
file |
diff |
annotate
|
Tue, 07 Sep 2010 16:40:30 +0200 |
wenzelm |
Isar_Document.reported_positions: slightly more robust treatment of positions outside the command range, notably parsing beyond EOF;
|
file |
diff |
annotate
|
Tue, 07 Sep 2010 15:03:59 +0200 |
wenzelm |
Isar_Document.reported_positions: exclude proof state output;
|
file |
diff |
annotate
|
Thu, 02 Sep 2010 23:26:21 +0200 |
wenzelm |
Isar_Document.reported_positions: more precise include/exclude, include root as last resort only;
|
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
|
Sun, 22 Aug 2010 20:11:17 +0200 |
wenzelm |
simplified Command.status again, reverting most of e5eed57913d0 (note that more complex information can be represented with full markup reports);
|
file |
diff |
annotate
|
Fri, 20 Aug 2010 11:57:43 +0200 |
wenzelm |
concentrate protocol message formats in Isar_Document;
|
file |
diff |
annotate
|
Thu, 19 Aug 2010 12:51:48 +0200 |
wenzelm |
moved Isar_Document to Pure/PIDE;
|
file |
diff |
annotate
| base
|