src/Pure/General/markup.ML
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;
2009-01-02 wenzelm 2009-01-02 added numeral, which supercedes num, xnum, float; renamed xstr to inner_string;
2008-11-29 nipkow 2008-11-29 New lexical item "float".
2008-09-03 wenzelm 2008-09-03 added const_decl;
2008-09-02 wenzelm 2008-09-02 added fixed_decl, fact_decl, local_fact_decl;
2008-08-28 wenzelm 2008-08-28 removed obsolete get_string; moved get_int to property.ML;
2008-08-27 wenzelm 2008-08-27 type Properties.T;
2008-08-23 wenzelm 2008-08-23 added messages and process information;
2008-08-15 wenzelm 2008-08-15 added ML_antiq, doc_antiq;
2008-08-15 wenzelm 2008-08-15 added is_none; added inner_comment;
2008-08-14 wenzelm 2008-08-14 tuned;
2008-08-14 wenzelm 2008-08-14 added ML_source, doc_source;
2008-08-13 wenzelm 2008-08-13 tuned;
2008-08-12 wenzelm 2008-08-12 renamed unknown_span to malformed_span; added ident; tuned;