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