| 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
|