src/Pure/General/markup.ML
Tue, 05 Jul 2011 22:39:15 +0200 wenzelm Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;
Tue, 05 Jul 2011 11:16:37 +0200 wenzelm tuned signature;
Wed, 29 Jun 2011 16:31:50 +0200 wenzelm print Path.T with some markup;
Mon, 27 Jun 2011 22:20:49 +0200 wenzelm document antiquotations are managed as theory data, with proper name space and entity markup;
Mon, 27 Jun 2011 16:53:31 +0200 wenzelm ML antiquotations are managed as theory data, with proper name space and entity markup;
Sat, 25 Jun 2011 19:38:35 +0200 wenzelm entity markup for "type", "constant";
Sat, 25 Jun 2011 18:15:36 +0200 wenzelm type classes: entity markup instead of old-style token markup;
Sat, 25 Jun 2011 17:17:49 +0200 wenzelm clarified Binding.pretty/print: no quotes, only markup -- Binding.str_of is rendered obsolete;
Sat, 18 Jun 2011 12:37:42 +0200 wenzelm inner literal/delimiter corresponds to outer keyword/operator;
Wed, 27 Apr 2011 20:28:27 +0200 wenzelm discontinued obsolete markup;
Sun, 17 Apr 2011 21:17:45 +0200 wenzelm markup attributes/methods via name space;
Sun, 17 Apr 2011 20:58:43 +0200 wenzelm markup facts via name space;
Sun, 17 Apr 2011 20:25:10 +0200 wenzelm tuned -- order in memory according to variance;
Sun, 17 Apr 2011 20:15:46 +0200 wenzelm eliminated obsolete markup -- superseded by generic "entity" markup;
Mon, 11 Apr 2011 17:11:03 +0200 wenzelm Name_Space.entry_markup: keep def position as separate properties;
Sun, 27 Mar 2011 20:55:01 +0200 wenzelm decode_term: some context-sensitive markup;
Sun, 20 Mar 2011 21:28:11 +0100 wenzelm structure Timing: covers former start_timing/end_timing and Output.timeit etc;
Sun, 09 Jan 2011 20:30:47 +0100 wenzelm more direct treatment of Position.end_offset;
Sun, 09 Jan 2011 16:03:56 +0100 wenzelm discontinued unused end_line, end_column;
Sat, 06 Nov 2010 18:10:35 +0100 wenzelm somewhat more uniform timing markup in ML vs. Scala;
Sat, 06 Nov 2010 16:31:35 +0100 wenzelm explicit "timing" status for toplevel transactions;
Mon, 25 Oct 2010 20:24:13 +0200 wenzelm explicitly qualify type Output.output, which is a slightly odd internal feature;
Wed, 22 Sep 2010 13:47:48 +0200 wenzelm main Isabelle_Process via Isabelle_System.Managed_Process;
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;
Tue, 07 Sep 2010 16:08:29 +0200 wenzelm highlight bad range of nested error (here from inner parsing);
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;
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 11:35:17 +0200 wenzelm message serial number indicates physical order;
Wed, 25 Aug 2010 21:31:22 +0200 wenzelm added some proof state markup, notably number of subgoals (e.g. for indentation);
Wed, 18 Aug 2010 11:02:47 +0200 wenzelm uniform Markup.empty/Markup.Empty in ML and Scala;
Mon, 16 Aug 2010 00:07:28 +0200 wenzelm simplified command status: interpret stacked markup on demand;
Sat, 14 Aug 2010 22:45:23 +0200 wenzelm more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
Sat, 07 Aug 2010 21:22:39 +0200 wenzelm more robust treatment of Markup.token;
Sun, 30 May 2010 16:00:13 +0200 wenzelm separate markup for ML delimiters;
Sun, 30 May 2010 14:21:35 +0200 wenzelm simplified command/keyword markup;
Sun, 30 May 2010 14:14:30 +0200 wenzelm markup non-identifier keyword as operator;
Sat, 29 May 2010 19:46:29 +0200 wenzelm explicit markup for forked goals, as indicated by Goal.fork;
Mon, 04 Jan 2010 18:56:36 +0100 wenzelm explicit markup of document assigment message (simplified variant of earlier "edits" 8c3e1f73953d);
Wed, 30 Dec 2009 22:56:46 +0100 wenzelm simplified init message -- removed redundant session property;
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;
Sat, 05 Dec 2009 16:39:49 +0100 wenzelm added markup for hidden text;
Thu, 12 Nov 2009 22:02:11 +0100 wenzelm eliminated obsolete "internal" kind -- collapsed to unspecific "";
Sun, 25 Oct 2009 20:54:21 +0100 wenzelm maintain theory name via name space, not tags;
Sun, 25 Oct 2009 19:18:59 +0100 wenzelm maintain group via name space, not tags;
Sun, 25 Oct 2009 13:18:35 +0100 wenzelm conceal consts via name space, not tags;
Sat, 24 Oct 2009 17:49:44 +0200 wenzelm markup for formal entities, with "def" or "ref" occurrences;
Tue, 29 Sep 2009 11:49:22 +0200 wenzelm explicit indication of Unsynchronized.ref;
Sat, 06 Jun 2009 19:58:10 +0200 wenzelm added markup ML_open, ML_struct;
Tue, 02 Jun 2009 23:30:45 +0200 wenzelm IsabelleProcess: emit status "ready" after initialization and reports;
Tue, 24 Mar 2009 15:43:13 +0100 wenzelm more markup elements for ML programs;
Fri, 20 Mar 2009 20:22:13 +0100 wenzelm report markup for ML tokens;
Tue, 03 Mar 2009 17:42:30 +0100 wenzelm added markup for binding;
Fri, 16 Jan 2009 22:56:12 +0100 wenzelm moved message markup into Scala layer -- reduced redundancy;
Thu, 15 Jan 2009 11:53:49 +0100 wenzelm replaced command_state by edits/edit;
Thu, 15 Jan 2009 00:41:24 +0100 wenzelm added command_state markup;
Fri, 09 Jan 2009 23:33:59 +0100 wenzelm added running task markup;
Fri, 02 Jan 2009 22:54:04 +0100 wenzelm Markup.no_output;
Fri, 02 Jan 2009 19:38:13 +0100 wenzelm added numeral, which supercedes num, xnum, float;
Sat, 29 Nov 2008 13:37:13 +0100 nipkow New lexical item "float".
Wed, 03 Sep 2008 17:47:37 +0200 wenzelm added const_decl;
less more (0) -100 -60 tip