| Mon, 23 Nov 2020 15:14:58 +0100 |
wenzelm |
support for PIDE markup in batch build (inactive due to pide_reports=false);
|
file |
diff |
annotate
|
| Sat, 26 May 2018 13:34:44 +0200 |
wenzelm |
tuned output;
|
file |
diff |
annotate
|
| Fri, 16 Mar 2018 17:16:09 +0100 |
wenzelm |
JSON representation for Position.T;
|
file |
diff |
annotate
|
| Thu, 06 Apr 2017 13:30:46 +0200 |
wenzelm |
proper default (amending 601866c61ded);
|
file |
diff |
annotate
|
| Sat, 31 Dec 2016 21:00:43 +0100 |
wenzelm |
more precise markup;
|
file |
diff |
annotate
|
| Fri, 23 Dec 2016 19:19:59 +0100 |
wenzelm |
full range for Position.Item;
|
file |
diff |
annotate
|
| Fri, 23 Dec 2016 11:53:31 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 15 Mar 2015 22:05:08 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 15 Mar 2015 21:57:10 +0100 |
wenzelm |
proper command id for inlined errors, which is important for Command.State.accumulate;
|
file |
diff |
annotate
|
| Tue, 10 Mar 2015 20:12:30 +0100 |
wenzelm |
more precise position information in Isabelle/Scala, with YXML markup as in Isabelle/ML;
|
file |
diff |
annotate
|
| Wed, 13 Aug 2014 22:29:43 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 12 Aug 2014 15:31:24 +0200 |
wenzelm |
clarified Position.Identified: do not require range from prover, default to command position;
|
file |
diff |
annotate
|
| Tue, 12 Aug 2014 14:15:58 +0200 |
wenzelm |
maintain Command_Range position as in ML;
|
file |
diff |
annotate
|
| Sat, 26 Apr 2014 13:34:10 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 11 Apr 2014 09:36:38 +0200 |
wenzelm |
tuned message, to accommodate extra brackets produced by Scala parsers;
|
file |
diff |
annotate
|
| Tue, 08 Apr 2014 20:03:00 +0200 |
wenzelm |
simplified Text.Chunk -- eliminated ooddities;
|
file |
diff |
annotate
|
| Tue, 08 Apr 2014 15:12:54 +0200 |
wenzelm |
tuned signature -- moved Command.Chunk to Text.Chunk;
|
file |
diff |
annotate
|
| Tue, 08 Apr 2014 13:24:08 +0200 |
wenzelm |
more precise token positions;
|
file |
diff |
annotate
|
| Tue, 08 Apr 2014 12:19:33 +0200 |
wenzelm |
more explicit Command.Chunk types, less ooddities;
|
file |
diff |
annotate
|
| Mon, 03 Mar 2014 12:54:12 +0100 |
wenzelm |
tuned signature -- emphasize symbol positions (prover) vs. decoded text offsets (editor);
|
file |
diff |
annotate
|
| Tue, 18 Feb 2014 18:43:47 +0100 |
wenzelm |
prefer concrete list append;
|
file |
diff |
annotate
|
| Fri, 14 Feb 2014 14:51:38 +0100 |
wenzelm |
updated thy_info.dependencies;
|
file |
diff |
annotate
|
| Tue, 11 Feb 2014 15:05:13 +0100 |
wenzelm |
report (but ignore) markup within auxiliary files;
|
file |
diff |
annotate
|
| Sun, 25 Nov 2012 19:49:24 +0100 |
wenzelm |
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
|
file |
diff |
annotate
|
| Tue, 18 Sep 2012 19:33:45 +0200 |
wenzelm |
pass base_snapshot to enable hyperlinks into other nodes;
|
file |
diff |
annotate
|
| Wed, 29 Aug 2012 11:48:45 +0200 |
wenzelm |
renamed Position.str_of to Position.here;
|
file |
diff |
annotate
|
| Fri, 24 Aug 2012 16:43:37 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 27 Jul 2012 14:09:59 +0200 |
wenzelm |
simplified Path vs. JVM File operations;
|
file |
diff |
annotate
|
| Fri, 20 Jul 2012 22:29:25 +0200 |
wenzelm |
more explicit java.io.{File => JFile};
|
file |
diff |
annotate
|
| Fri, 20 Jul 2012 18:50:33 +0200 |
wenzelm |
require explicit initialization of options;
|
file |
diff |
annotate
|
| Mon, 28 Nov 2011 22:05:32 +0100 |
wenzelm |
separate module for concrete Isabelle markup;
|
file |
diff |
annotate
|
| Tue, 12 Jul 2011 19:36:46 +0200 |
wenzelm |
more uniform Properties in ML and Scala;
|
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
|
| Mon, 11 Apr 2011 17:11:03 +0200 |
wenzelm |
Name_Space.entry_markup: keep def position as separate properties;
|
file |
diff |
annotate
|
| Sun, 09 Jan 2011 16:03:56 +0100 |
wenzelm |
discontinued unused end_line, end_column;
|
file |
diff |
annotate
|
| Thu, 02 Sep 2010 23:17:13 +0200 |
wenzelm |
Position.Range: exclude singularity (again);
|
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
|
| Wed, 25 Aug 2010 22:37:53 +0200 |
wenzelm |
organized markup properties via apply/unapply patterns;
|
file |
diff |
annotate
|
| Fri, 20 Aug 2010 12:12:28 +0200 |
wenzelm |
alternative constructor for Range singularities;
|
file |
diff |
annotate
|
| Fri, 20 Aug 2010 11:00:15 +0200 |
wenzelm |
further clarification/unification of Position.Range and Text.Range concerning singularities: start offset is always included;
|
file |
diff |
annotate
|
| Wed, 18 Aug 2010 23:44:50 +0200 |
wenzelm |
more efficient Markup_Tree, based on branches sorted by quasi-order;
|
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
|
| Thu, 06 May 2010 16:27:47 +0200 |
wenzelm |
basic support for symbolic pretty printing;
|
file |
diff |
annotate
|
| Wed, 05 May 2010 23:09:34 +0200 |
wenzelm |
simplified via Position extractors;
|
file |
diff |
annotate
|
| Wed, 30 Dec 2009 20:25:35 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 29 Aug 2009 14:31:39 +0200 |
wenzelm |
misc tuning;
|
file |
diff |
annotate
|
| Thu, 18 Jun 2009 19:03:39 +0200 |
wenzelm |
replaced java Properties by pure property lists;
|
file |
diff |
annotate
|
| Fri, 19 Dec 2008 20:37:29 +0100 |
wenzelm |
removed Ids;
|
file |
diff |
annotate
|
| Mon, 25 Aug 2008 20:01:17 +0200 |
wenzelm |
simplified exceptions: use plain error function / RuntimeException;
|
file |
diff |
annotate
|
| Sun, 24 Aug 2008 21:15:44 +0200 |
wenzelm |
get: allow null;
|
file |
diff |
annotate
|
| Sat, 23 Aug 2008 23:07:36 +0200 |
wenzelm |
Position properties.
|
file |
diff |
annotate
|