| Mon, 28 Nov 2011 22:05:32 +0100 |
wenzelm |
separate module for concrete Isabelle markup;
|
file |
diff |
annotate
|
| Sat, 15 Oct 2011 15:55:10 +0200 |
wenzelm |
updated to polyml-5.4.1;
|
file |
diff |
annotate
|
| Tue, 06 Sep 2011 20:55:18 +0200 |
wenzelm |
bulk reports for improved message throughput;
|
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
|
| Tue, 11 Jan 2011 16:23:28 +0100 |
wenzelm |
clarified notion Position.is_reported;
|
file |
diff |
annotate
|
| Mon, 10 Jan 2011 22:03:24 +0100 |
wenzelm |
refined report_parse_tree: reverse reports happen to produce proper type information for inlined @{term}, @{typ} etc.;
|
file |
diff |
annotate
|
| Mon, 10 Jan 2011 21:21:23 +0100 |
wenzelm |
ML compiler: more careful treatment of input tokens -- trailing space ensures proper separation and end position (cf. 82c1e348bc18, 08240feb69c7);
|
file |
diff |
annotate
|
| Sun, 09 Jan 2011 20:30:47 +0100 |
wenzelm |
more direct treatment of Position.end_offset;
|
file |
diff |
annotate
|
| Sun, 09 Jan 2011 16:03:56 +0100 |
wenzelm |
discontinued unused end_line, end_column;
|
file |
diff |
annotate
|
| Sun, 28 Nov 2010 20:36:45 +0100 |
wenzelm |
ML results: enter before printing (cf. Poly/ML SVN 1218);
|
file |
diff |
annotate
|
| Fri, 17 Sep 2010 20:18:27 +0200 |
wenzelm |
tuned signature of (Context_)Position.report variants;
|
file |
diff |
annotate
|
| Fri, 17 Sep 2010 17:09:31 +0200 |
wenzelm |
simplified/clarified (Context_)Position.markup/reported_text;
|
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
|
| Thu, 09 Sep 2010 20:09:13 +0200 |
wenzelm |
ML_Compiler.eval: reported positions need to contain offset, to avoid displaced reports due to synthesized line numbers;
|
file |
diff |
annotate
|
| Thu, 09 Sep 2010 17:20:27 +0200 |
wenzelm |
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
|
file |
diff |
annotate
|
| Thu, 09 Sep 2010 11:05:52 +0200 |
wenzelm |
avoid mixing of static and runtime errors in compiler output, to accomodate Proof General;
|
file |
diff |
annotate
|
| Wed, 08 Sep 2010 23:52:24 +0200 |
wenzelm |
ML_Compiler.eval: discontinued extra "Static Errors" of raw Poly/ML;
|
file |
diff |
annotate
|
| Wed, 08 Sep 2010 23:34:40 +0200 |
wenzelm |
ML_Compiler.eval: more careful printing of messages and regular output, trying to accomodate Poly/ML, Proof General, Isabelle/Scala/jEdit at the same time;
|
file |
diff |
annotate
|
| Wed, 08 Sep 2010 22:30:29 +0200 |
wenzelm |
clarified -- inlined ML_Env.local_context;
|
file |
diff |
annotate
|
| Mon, 30 Aug 2010 15:09:20 +0200 |
wenzelm |
more careful treatment of nested multi-exceptions, collapsing cumulatively empty list to Interrupt;
|
file |
diff |
annotate
|
| Wed, 25 Aug 2010 20:43:03 +0200 |
wenzelm |
ML_Context.eval: produce antiquotation environment preferably in invisible context, to avoid displaced report messages from ML_Compiler;
|
file |
diff |
annotate
|
| Sat, 07 Aug 2010 21:03:06 +0200 |
wenzelm |
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
|
file |
diff |
annotate
|
| Mon, 31 May 2010 18:17:48 +0200 |
wenzelm |
terminate ML compiler input produced by ML_Lex.read (cf. 85e864045497);
|
file |
diff |
annotate
|
| Tue, 10 Nov 2009 23:15:20 +0100 |
wenzelm |
generalized Runtime.toplevel_error wrt. output function;
|
file |
diff |
annotate
|
| Mon, 09 Nov 2009 21:30:54 +0100 |
wenzelm |
setup for official Poly/ML 5.3.0, which is now the default;
|
file |
diff |
annotate
|
| Tue, 29 Sep 2009 11:49:22 +0200 |
wenzelm |
explicit indication of Unsynchronized.ref;
|
file |
diff |
annotate
|
| Wed, 02 Sep 2009 17:33:25 +0200 |
wenzelm |
updated Poly/ML SVN version;
|
file |
diff |
annotate
|
| Wed, 02 Sep 2009 16:51:19 +0200 |
wenzelm |
eval/location_props: always produce YXML markup, independent of print_mode;
|
file |
diff |
annotate
|
| Wed, 02 Sep 2009 14:11:45 +0200 |
wenzelm |
tuned ML message;
|
file |
diff |
annotate
|
| Mon, 22 Jun 2009 22:49:44 +0200 |
wenzelm |
eval: tuned input buffer and get_offset (which ran very hot, up to the point where AFP/FlyspeckTame would seemingly take forever);
|
file |
diff |
annotate
|
| Sat, 06 Jun 2009 21:57:50 +0200 |
wenzelm |
updated version;
|
file |
diff |
annotate
|
| Sat, 06 Jun 2009 21:47:02 +0200 |
wenzelm |
reraise exceptions to preserve position information;
|
file |
diff |
annotate
|
| Sat, 06 Jun 2009 21:11:23 +0200 |
wenzelm |
added exn_message (formerly in toplevel.ML);
|
file |
diff |
annotate
|
| Sat, 06 Jun 2009 19:58:11 +0200 |
wenzelm |
report_parse_tree: ML_open, ML_struct;
|
file |
diff |
annotate
|
| Thu, 04 Jun 2009 22:02:33 +0200 |
wenzelm |
removed unused location_of;
|
file |
diff |
annotate
|
| Thu, 04 Jun 2009 19:15:55 +0200 |
wenzelm |
more robust treatment of bootstrap source positions;
|
file |
diff |
annotate
|
| Thu, 04 Jun 2009 17:31:38 +0200 |
wenzelm |
convert explicitly between Position.T/PolyML.location, without costly registration of tokens;
|
file |
diff |
annotate
|
| Mon, 01 Jun 2009 23:28:06 +0200 |
wenzelm |
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
|
file |
diff |
annotate
|