| Mon, 28 Nov 2011 22:05:32 +0100 |
wenzelm |
separate module for concrete Isabelle markup;
|
file |
diff |
annotate
|
| Thu, 10 Nov 2011 22:32:10 +0100 |
wenzelm |
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
|
file |
diff |
annotate
|
| Sun, 04 Sep 2011 19:36:19 +0200 |
wenzelm |
eliminated markup for plain identifiers (frequent but insignificant);
|
file |
diff |
annotate
|
| Sat, 03 Sep 2011 21:15:35 +0200 |
wenzelm |
Document.removed_versions on Scala side;
|
file |
diff |
annotate
|
| Fri, 02 Sep 2011 21:48:27 +0200 |
wenzelm |
raw message function "assign_execs" avoids full overhead of decoding and caching message body;
|
file |
diff |
annotate
|
| Sat, 27 Aug 2011 17:26:14 +0200 |
wenzelm |
explicit markup for legacy warnings;
|
file |
diff |
annotate
|
| Thu, 25 Aug 2011 16:44:06 +0200 |
wenzelm |
propagate information about last command with exec state assignment through document model;
|
file |
diff |
annotate
|
| Fri, 19 Aug 2011 14:01:20 +0200 |
wenzelm |
Future.promise: explicit abort operation (like uninterruptible future job);
|
file |
diff |
annotate
|
| Thu, 14 Jul 2011 22:30:31 +0200 |
wenzelm |
more precise integer Markup.properties/XML.attributes: disallow ML-style ~ minus;
|
file |
diff |
annotate
|
| Mon, 11 Jul 2011 16:48:02 +0200 |
wenzelm |
JVM method invocation service via Scala layer;
|
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
|
| Wed, 06 Jul 2011 20:46:06 +0200 |
wenzelm |
prefer Synchronized.var;
|
file |
diff |
annotate
|
| Tue, 05 Jul 2011 22:39:15 +0200 |
wenzelm |
Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;
|
file |
diff |
annotate
|
| Tue, 05 Jul 2011 11:16:37 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 29 Jun 2011 16:31:50 +0200 |
wenzelm |
print Path.T with some markup;
|
file |
diff |
annotate
|
| Mon, 27 Jun 2011 22:20:49 +0200 |
wenzelm |
document antiquotations are managed as theory data, with proper name space and entity markup;
|
file |
diff |
annotate
|
| Mon, 27 Jun 2011 16:53:31 +0200 |
wenzelm |
ML antiquotations are managed as theory data, with proper name space and entity markup;
|
file |
diff |
annotate
|
| Sat, 25 Jun 2011 19:38:35 +0200 |
wenzelm |
entity markup for "type", "constant";
|
file |
diff |
annotate
|
| Sat, 25 Jun 2011 18:15:36 +0200 |
wenzelm |
type classes: entity markup instead of old-style token markup;
|
file |
diff |
annotate
|
| Sat, 25 Jun 2011 17:17:49 +0200 |
wenzelm |
clarified Binding.pretty/print: no quotes, only markup -- Binding.str_of is rendered obsolete;
|
file |
diff |
annotate
|
| Sat, 18 Jun 2011 12:37:42 +0200 |
wenzelm |
inner literal/delimiter corresponds to outer keyword/operator;
|
file |
diff |
annotate
|
| Wed, 27 Apr 2011 20:28:27 +0200 |
wenzelm |
discontinued obsolete markup;
|
file |
diff |
annotate
|
| Sun, 17 Apr 2011 21:17:45 +0200 |
wenzelm |
markup attributes/methods via name space;
|
file |
diff |
annotate
|
| Sun, 17 Apr 2011 20:58:43 +0200 |
wenzelm |
markup facts via name space;
|
file |
diff |
annotate
|
| Sun, 17 Apr 2011 20:25:10 +0200 |
wenzelm |
tuned -- order in memory according to variance;
|
file |
diff |
annotate
|
| Sun, 17 Apr 2011 20:15:46 +0200 |
wenzelm |
eliminated obsolete markup -- superseded by generic "entity" markup;
|
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, 27 Mar 2011 20:55:01 +0200 |
wenzelm |
decode_term: some context-sensitive markup;
|
file |
diff |
annotate
|
| Sun, 20 Mar 2011 21:28:11 +0100 |
wenzelm |
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
|
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
|
| Sat, 06 Nov 2010 18:10:35 +0100 |
wenzelm |
somewhat more uniform timing markup in ML vs. Scala;
|
file |
diff |
annotate
|
| Sat, 06 Nov 2010 16:31:35 +0100 |
wenzelm |
explicit "timing" status for toplevel transactions;
|
file |
diff |
annotate
|
| Mon, 25 Oct 2010 20:24:13 +0200 |
wenzelm |
explicitly qualify type Output.output, which is a slightly odd internal feature;
|
file |
diff |
annotate
|
| Wed, 22 Sep 2010 13:47:48 +0200 |
wenzelm |
main Isabelle_Process via Isabelle_System.Managed_Process;
|
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 16:08:29 +0200 |
wenzelm |
highlight bad range of nested error (here from inner parsing);
|
file |
diff |
annotate
|
| Tue, 07 Sep 2010 14:08:21 +0200 |
wenzelm |
report token range after inner parse error -- often provides important clues about misunderstanding concerning lexical phase;
|
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 11:35:17 +0200 |
wenzelm |
message serial number indicates physical order;
|
file |
diff |
annotate
|
| Wed, 25 Aug 2010 21:31:22 +0200 |
wenzelm |
added some proof state markup, notably number of subgoals (e.g. for indentation);
|
file |
diff |
annotate
|
| Wed, 18 Aug 2010 11:02:47 +0200 |
wenzelm |
uniform Markup.empty/Markup.Empty in ML and Scala;
|
file |
diff |
annotate
|
| Mon, 16 Aug 2010 00:07:28 +0200 |
wenzelm |
simplified command status: interpret stacked markup on demand;
|
file |
diff |
annotate
|
| Sat, 14 Aug 2010 22:45:23 +0200 |
wenzelm |
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
|
file |
diff |
annotate
|
| Sat, 07 Aug 2010 21:22:39 +0200 |
wenzelm |
more robust treatment of Markup.token;
|
file |
diff |
annotate
|
| Sun, 30 May 2010 16:00:13 +0200 |
wenzelm |
separate markup for ML delimiters;
|
file |
diff |
annotate
|
| Sun, 30 May 2010 14:21:35 +0200 |
wenzelm |
simplified command/keyword markup;
|
file |
diff |
annotate
|
| Sun, 30 May 2010 14:14:30 +0200 |
wenzelm |
markup non-identifier keyword as operator;
|
file |
diff |
annotate
|
| Sat, 29 May 2010 19:46:29 +0200 |
wenzelm |
explicit markup for forked goals, as indicated by Goal.fork;
|
file |
diff |
annotate
|
| Mon, 04 Jan 2010 18:56:36 +0100 |
wenzelm |
explicit markup of document assigment message (simplified variant of earlier "edits" 8c3e1f73953d);
|
file |
diff |
annotate
|
| Wed, 30 Dec 2009 22:56:46 +0100 |
wenzelm |
simplified init message -- removed redundant session property;
|
file |
diff |
annotate
|
| Wed, 30 Dec 2009 21:32:25 +0100 |
wenzelm |
eliminated Markup.edits/EDITS: Isar.edit_document reports Markup.edit/EDIT while running under new document id;
|
file |
diff |
annotate
|
| Sat, 05 Dec 2009 16:39:49 +0100 |
wenzelm |
added markup for hidden text;
|
file |
diff |
annotate
|
| Thu, 12 Nov 2009 22:02:11 +0100 |
wenzelm |
eliminated obsolete "internal" kind -- collapsed to unspecific "";
|
file |
diff |
annotate
|
| Sun, 25 Oct 2009 20:54:21 +0100 |
wenzelm |
maintain theory name via name space, not tags;
|
file |
diff |
annotate
|
| Sun, 25 Oct 2009 19:18:59 +0100 |
wenzelm |
maintain group via name space, not tags;
|
file |
diff |
annotate
|
| Sun, 25 Oct 2009 13:18:35 +0100 |
wenzelm |
conceal consts via name space, not tags;
|
file |
diff |
annotate
|
| Sat, 24 Oct 2009 17:49:44 +0200 |
wenzelm |
markup for formal entities, with "def" or "ref" occurrences;
|
file |
diff |
annotate
|
| Tue, 29 Sep 2009 11:49:22 +0200 |
wenzelm |
explicit indication of Unsynchronized.ref;
|
file |
diff |
annotate
|
| Sat, 06 Jun 2009 19:58:10 +0200 |
wenzelm |
added markup ML_open, ML_struct;
|
file |
diff |
annotate
|
| Tue, 02 Jun 2009 23:30:45 +0200 |
wenzelm |
IsabelleProcess: emit status "ready" after initialization and reports;
|
file |
diff |
annotate
|
| Tue, 24 Mar 2009 15:43:13 +0100 |
wenzelm |
more markup elements for ML programs;
|
file |
diff |
annotate
|
| Fri, 20 Mar 2009 20:22:13 +0100 |
wenzelm |
report markup for ML tokens;
|
file |
diff |
annotate
|
| Tue, 03 Mar 2009 17:42:30 +0100 |
wenzelm |
added markup for binding;
|
file |
diff |
annotate
|
| Fri, 16 Jan 2009 22:56:12 +0100 |
wenzelm |
moved message markup into Scala layer -- reduced redundancy;
|
file |
diff |
annotate
|
| Thu, 15 Jan 2009 11:53:49 +0100 |
wenzelm |
replaced command_state by edits/edit;
|
file |
diff |
annotate
|
| Thu, 15 Jan 2009 00:41:24 +0100 |
wenzelm |
added command_state markup;
|
file |
diff |
annotate
|
| Fri, 09 Jan 2009 23:33:59 +0100 |
wenzelm |
added running task markup;
|
file |
diff |
annotate
|
| Fri, 02 Jan 2009 22:54:04 +0100 |
wenzelm |
Markup.no_output;
|
file |
diff |
annotate
|
| Fri, 02 Jan 2009 19:38:13 +0100 |
wenzelm |
added numeral, which supercedes num, xnum, float;
|
file |
diff |
annotate
|
| Sat, 29 Nov 2008 13:37:13 +0100 |
nipkow |
New lexical item "float".
|
file |
diff |
annotate
|
| Wed, 03 Sep 2008 17:47:37 +0200 |
wenzelm |
added const_decl;
|
file |
diff |
annotate
|
| Tue, 02 Sep 2008 14:10:27 +0200 |
wenzelm |
added fixed_decl, fact_decl, local_fact_decl;
|
file |
diff |
annotate
|
| Thu, 28 Aug 2008 00:33:07 +0200 |
wenzelm |
removed obsolete get_string;
|
file |
diff |
annotate
|
| Wed, 27 Aug 2008 11:48:54 +0200 |
wenzelm |
type Properties.T;
|
file |
diff |
annotate
|
| Sat, 23 Aug 2008 23:07:38 +0200 |
wenzelm |
added messages and process information;
|
file |
diff |
annotate
|
| Fri, 15 Aug 2008 17:03:52 +0200 |
wenzelm |
added ML_antiq, doc_antiq;
|
file |
diff |
annotate
|
| Fri, 15 Aug 2008 15:50:49 +0200 |
wenzelm |
added is_none;
|
file |
diff |
annotate
|
| Thu, 14 Aug 2008 20:29:37 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 14 Aug 2008 20:13:40 +0200 |
wenzelm |
added ML_source, doc_source;
|
file |
diff |
annotate
|
| Wed, 13 Aug 2008 20:57:22 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 12 Aug 2008 21:27:51 +0200 |
wenzelm |
renamed unknown_span to malformed_span;
|
file |
diff |
annotate
|
| Mon, 11 Aug 2008 18:37:49 +0200 |
wenzelm |
renamed Markup.class to Markup.tclass, to avoid potential conflicts with spacial meaning in markup languages (e.g. HTML);
|
file |
diff |
annotate
|
| Sun, 10 Aug 2008 12:38:22 +0200 |
wenzelm |
added name property operation;
|
file |
diff |
annotate
|
| Sat, 09 Aug 2008 12:28:09 +0200 |
wenzelm |
added literal;
|
file |
diff |
annotate
|
| Fri, 08 Aug 2008 19:28:59 +0200 |
wenzelm |
added offset/end_offset;
|
file |
diff |
annotate
|
| Wed, 06 Aug 2008 00:10:08 +0200 |
wenzelm |
added position_properties';
|
file |
diff |
annotate
|
| Tue, 05 Aug 2008 19:29:02 +0200 |
wenzelm |
added token;
|
file |
diff |
annotate
|
| Tue, 05 Aug 2008 13:31:36 +0200 |
wenzelm |
removed axiom;
|
file |
diff |
annotate
|
| Mon, 04 Aug 2008 22:55:04 +0200 |
wenzelm |
added end_line, end_column properties;
|
file |
diff |
annotate
|
| Sun, 20 Jul 2008 23:06:53 +0200 |
wenzelm |
renamed command span markup;
|
file |
diff |
annotate
|
| Tue, 15 Jul 2008 23:36:26 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 15 Jul 2008 15:46:41 +0200 |
wenzelm |
support for command status;
|
file |
diff |
annotate
|
| Thu, 10 Jul 2008 17:26:22 +0200 |
wenzelm |
added prompt markup;
|
file |
diff |
annotate
|
| Fri, 23 May 2008 21:18:47 +0200 |
wenzelm |
added theory_nameN;
|
file |
diff |
annotate
|
| Thu, 17 Apr 2008 16:30:48 +0200 |
wenzelm |
added markup for fixed variables (local constants);
|
file |
diff |
annotate
|
| Tue, 11 Mar 2008 22:31:07 +0100 |
wenzelm |
added location;
|
file |
diff |
annotate
|
| Sun, 10 Feb 2008 20:49:45 +0100 |
wenzelm |
added position_properties;
|
file |
diff |
annotate
|
| Mon, 28 Jan 2008 22:27:21 +0100 |
wenzelm |
added column property;
|
file |
diff |
annotate
|
| Sat, 26 Jan 2008 17:08:41 +0100 |
wenzelm |
added theorem group property;
|
file |
diff |
annotate
|
| Sun, 06 Jan 2008 15:57:49 +0100 |
wenzelm |
removed obsolete prompt and channel markups;
|
file |
diff |
annotate
|
| Thu, 03 Jan 2008 22:25:11 +0100 |
wenzelm |
moved id to position properties;
|
file |
diff |
annotate
|
| Thu, 03 Jan 2008 17:50:42 +0100 |
wenzelm |
added id property;
|
file |
diff |
annotate
|
| Thu, 06 Dec 2007 00:21:32 +0100 |
wenzelm |
added channels;
|
file |
diff |
annotate
|
| Sat, 06 Oct 2007 17:46:49 +0200 |
wenzelm |
added keyword_decl, command_decl;
|
file |
diff |
annotate
|
| Sun, 30 Sep 2007 16:20:39 +0200 |
wenzelm |
added internalK, property_internal;
|
file |
diff |
annotate
|
| Mon, 17 Sep 2007 16:36:41 +0200 |
wenzelm |
avoid direct access to print_mode;
|
file |
diff |
annotate
|
| Fri, 07 Sep 2007 22:13:45 +0200 |
wenzelm |
added hilite markup;
|
file |
diff |
annotate
|
| Wed, 15 Aug 2007 19:24:23 +0200 |
wenzelm |
added sendback;
|
file |
diff |
annotate
|
| Mon, 23 Jul 2007 14:06:12 +0200 |
wenzelm |
marked some CRITICAL sections (for multithreading);
|
file |
diff |
annotate
|
| Thu, 12 Jul 2007 00:15:28 +0200 |
wenzelm |
added get_string, get_int;
|
file |
diff |
annotate
|
| Wed, 11 Jul 2007 17:47:48 +0200 |
wenzelm |
removed ident, space;
|
file |
diff |
annotate
|
| Tue, 10 Jul 2007 23:29:43 +0200 |
wenzelm |
more markup for inner and outer syntax;
|
file |
diff |
annotate
|
| Tue, 10 Jul 2007 16:46:37 +0200 |
wenzelm |
added print_mode setup (from pretty.ML);
|
file |
diff |
annotate
|
| Tue, 10 Jul 2007 15:45:34 +0200 |
aspinall |
Add widthN to signature
|
file |
diff |
annotate
|
| Mon, 09 Jul 2007 23:12:35 +0200 |
wenzelm |
proper position markup;
|
file |
diff |
annotate
|
| Sun, 08 Jul 2007 19:52:08 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 08 Jul 2007 13:10:51 +0200 |
wenzelm |
added markup for pretty printing;
|
file |
diff |
annotate
|
| Sat, 07 Jul 2007 18:47:47 +0200 |
wenzelm |
make smlnj happy;
|
file |
diff |
annotate
|
| Sat, 07 Jul 2007 18:39:17 +0200 |
wenzelm |
added toplevel markup;
|
file |
diff |
annotate
|