src/Pure/General/position.scala
Tue, 10 Mar 2015 20:12:30 +0100 wenzelm more precise position information in Isabelle/Scala, with YXML markup as in Isabelle/ML;
Wed, 13 Aug 2014 22:29:43 +0200 wenzelm tuned;
Tue, 12 Aug 2014 15:31:24 +0200 wenzelm clarified Position.Identified: do not require range from prover, default to command position;
Tue, 12 Aug 2014 14:15:58 +0200 wenzelm maintain Command_Range position as in ML;
Sat, 26 Apr 2014 13:34:10 +0200 wenzelm tuned signature;
Fri, 11 Apr 2014 09:36:38 +0200 wenzelm tuned message, to accommodate extra brackets produced by Scala parsers;
Tue, 08 Apr 2014 20:03:00 +0200 wenzelm simplified Text.Chunk -- eliminated ooddities;
Tue, 08 Apr 2014 15:12:54 +0200 wenzelm tuned signature -- moved Command.Chunk to Text.Chunk;
Tue, 08 Apr 2014 13:24:08 +0200 wenzelm more precise token positions;
Tue, 08 Apr 2014 12:19:33 +0200 wenzelm more explicit Command.Chunk types, less ooddities;
Mon, 03 Mar 2014 12:54:12 +0100 wenzelm tuned signature -- emphasize symbol positions (prover) vs. decoded text offsets (editor);
Tue, 18 Feb 2014 18:43:47 +0100 wenzelm prefer concrete list append;
Fri, 14 Feb 2014 14:51:38 +0100 wenzelm updated thy_info.dependencies;
Tue, 11 Feb 2014 15:05:13 +0100 wenzelm report (but ignore) markup within auxiliary files;
Sun, 25 Nov 2012 19:49:24 +0100 wenzelm Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
Tue, 18 Sep 2012 19:33:45 +0200 wenzelm pass base_snapshot to enable hyperlinks into other nodes;
Wed, 29 Aug 2012 11:48:45 +0200 wenzelm renamed Position.str_of to Position.here;
Fri, 24 Aug 2012 16:43:37 +0200 wenzelm tuned signature;
Fri, 27 Jul 2012 14:09:59 +0200 wenzelm simplified Path vs. JVM File operations;
Fri, 20 Jul 2012 22:29:25 +0200 wenzelm more explicit java.io.{File => JFile};
Fri, 20 Jul 2012 18:50:33 +0200 wenzelm require explicit initialization of options;
Mon, 28 Nov 2011 22:05:32 +0100 wenzelm separate module for concrete Isabelle markup;
Tue, 12 Jul 2011 19:36:46 +0200 wenzelm more uniform Properties in ML and Scala;
Fri, 08 Jul 2011 17:04:38 +0200 wenzelm discontinued odd Position.column -- left-over from attempts at PGIP implementation;
Mon, 11 Apr 2011 17:11:03 +0200 wenzelm Name_Space.entry_markup: keep def position as separate properties;
Sun, 09 Jan 2011 16:03:56 +0100 wenzelm discontinued unused end_line, end_column;
Thu, 02 Sep 2010 23:17:13 +0200 wenzelm Position.Range: exclude singularity (again);
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;
Wed, 25 Aug 2010 22:37:53 +0200 wenzelm organized markup properties via apply/unapply patterns;
less more (0) -30 tip