src/Pure/General/markup.ML
2011-07-11 wenzelm 2011-07-11 JVM method invocation service via Scala layer;
2011-07-08 wenzelm 2011-07-08 discontinued odd Position.column -- left-over from attempts at PGIP implementation; Position.offset discriminates postions precisely, now also available for Position.line/line_file;
2011-07-06 wenzelm 2011-07-06 prefer Synchronized.var;
2011-07-05 wenzelm 2011-07-05 Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;
2011-07-05 wenzelm 2011-07-05 tuned signature; tuned;
2011-06-29 wenzelm 2011-06-29 print Path.T with some markup;
2011-06-27 wenzelm 2011-06-27 document antiquotations are managed as theory data, with proper name space and entity markup;
2011-06-27 wenzelm 2011-06-27 ML antiquotations are managed as theory data, with proper name space and entity markup; clarified Name_Space.check;
2011-06-25 wenzelm 2011-06-25 entity markup for "type", "constant";
2011-06-25 wenzelm 2011-06-25 type classes: entity markup instead of old-style token markup;
2011-06-25 wenzelm 2011-06-25 clarified Binding.pretty/print: no quotes, only markup -- Binding.str_of is rendered obsolete;
2011-06-18 wenzelm 2011-06-18 inner literal/delimiter corresponds to outer keyword/operator;
2011-04-27 wenzelm 2011-04-27 discontinued obsolete markup;
2011-04-17 wenzelm 2011-04-17 markup attributes/methods via name space; eliminated obsolete markup;
2011-04-17 wenzelm 2011-04-17 markup facts via name space; eliminated obsolete markup;
2011-04-17 wenzelm 2011-04-17 tuned -- order in memory according to variance;
2011-04-17 wenzelm 2011-04-17 eliminated obsolete markup -- superseded by generic "entity" markup;
2011-04-11 wenzelm 2011-04-11 Name_Space.entry_markup: keep def position as separate properties; uniform treatment of ML_def/ML_open/ML_struct as entities; hyperlinks for all entities -- excluding ML_open/ML_struct for now;
2011-03-27 wenzelm 2011-03-27 decode_term: some context-sensitive markup; more informative Markup.entity and Name_Space.markup_entry; Markup.const: use "constant" to make it coincide with name space kind;
2011-03-20 wenzelm 2011-03-20 structure Timing: covers former start_timing/end_timing and Output.timeit etc; explicit Timing.message function; eliminated Output.timing flag, cf. Toplevel.timing; tuned;
2011-01-09 wenzelm 2011-01-09 more direct treatment of Position.end_offset; tuned;
2011-01-09 wenzelm 2011-01-09 discontinued unused end_line, end_column;
2010-11-06 wenzelm 2010-11-06 somewhat more uniform timing markup in ML vs. Scala;
2010-11-06 wenzelm 2010-11-06 explicit "timing" status for toplevel transactions;
2010-10-25 wenzelm 2010-10-25 explicitly qualify type Output.output, which is a slightly odd internal feature;
2010-09-22 wenzelm 2010-09-22 main Isabelle_Process via Isabelle_System.Managed_Process; simplified init message: no pid; misc tuning and simplification;
2010-09-17 wenzelm 2010-09-17 eliminated markup "location" in favour of more explicit "no_report", which is actually deleted from messages;
2010-09-07 wenzelm 2010-09-07 highlight bad range of nested error (here from inner parsing);
2010-09-07 wenzelm 2010-09-07 report token range after inner parse error -- often provides important clues about misunderstanding concerning lexical phase; tuned color;
2010-08-31 wenzelm 2010-08-31 Command.State: add reported positions to markup tree, according main message position or Markup.binding/entity/report occurrences in body; Position.Id_Range convenience;
2010-08-30 wenzelm 2010-08-30 message serial number indicates physical order;
2010-08-25 wenzelm 2010-08-25 added some proof state markup, notably number of subgoals (e.g. for indentation); tuned;
2010-08-18 wenzelm 2010-08-18 uniform Markup.empty/Markup.Empty in ML and Scala;
2010-08-16 wenzelm 2010-08-16 simplified command status: interpret stacked markup on demand;
2010-08-14 wenzelm 2010-08-14 more basic Markup.parse_int/print_int (using signed_string_of_int) (ML); added convenient Markup.Int/Long objects (Scala); simplified "assign" message format -- explicit version id; misc tuning and simplification;
2010-08-07 wenzelm 2010-08-07 more robust treatment of Markup.token;
2010-05-30 wenzelm 2010-05-30 separate markup for ML delimiters;
2010-05-30 wenzelm 2010-05-30 simplified command/keyword markup;
2010-05-30 wenzelm 2010-05-30 markup non-identifier keyword as operator;
2010-05-29 wenzelm 2010-05-29 explicit markup for forked goals, as indicated by Goal.fork; accumulate pending forks within command state and hilight accordingly; Isabelle_Process: enforce future_terminal_proof, which gives some impression of non-linear/parallel checking;
2010-01-04 wenzelm 2010-01-04 explicit markup of document assigment message (simplified variant of earlier "edits" 8c3e1f73953d);
2009-12-30 wenzelm 2009-12-30 simplified init message -- removed redundant session property;
2009-12-30 wenzelm 2009-12-30 eliminated Markup.edits/EDITS: Isar.edit_document reports Markup.edit/EDIT while running under new document id; eliminated ML interface of Isar_Document: the protocol only works with certain transaction positions, i.e. via Isar commands;
2009-12-05 wenzelm 2009-12-05 added markup for hidden text; handle "\<^bold>" as markup; HTML output: include original control symbols as hidden text, to enable copy-paste;
2009-11-12 wenzelm 2009-11-12 eliminated obsolete "internal" kind -- collapsed to unspecific "";
2009-10-25 wenzelm 2009-10-25 maintain theory name via name space, not tags; AxClass.thynames_of_arity: explicit theory name, not tags;
2009-10-25 wenzelm 2009-10-25 maintain group via name space, not tags;
2009-10-25 wenzelm 2009-10-25 conceal consts via name space, not tags;
2009-10-24 wenzelm 2009-10-24 markup for formal entities, with "def" or "ref" occurrences;
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-06-06 wenzelm 2009-06-06 added markup ML_open, ML_struct;
2009-06-02 wenzelm 2009-06-02 IsabelleProcess: emit status "ready" after initialization and reports;
2009-03-24 wenzelm 2009-03-24 more markup elements for ML programs;
2009-03-20 wenzelm 2009-03-20 report markup for ML tokens;
2009-03-03 wenzelm 2009-03-03 added markup for binding; tuned;
2009-01-16 wenzelm 2009-01-16 moved message markup into Scala layer -- reduced redundancy;
2009-01-15 wenzelm 2009-01-15 replaced command_state by edits/edit;
2009-01-15 wenzelm 2009-01-15 added command_state markup;
2009-01-09 wenzelm 2009-01-09 added running task markup;
2009-01-02 wenzelm 2009-01-02 Markup.no_output;