src/Pure/General/markup.scala
2010-08-30 wenzelm 2010-08-30 Command.results: ordered by serial number;
2010-08-30 wenzelm 2010-08-30 message serial number indicates physical order;
2010-08-25 wenzelm 2010-08-25 Pretty: tuned markup objects;
2010-08-25 wenzelm 2010-08-25 organized markup properties via apply/unapply patterns;
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-11 wenzelm 2010-08-11 represent document ids by (long) int, to benefit from the somewhat faster Inttab in ML (LinearSet in Scala is invariably indexed by native object ids);
2010-08-10 wenzelm 2010-08-10 distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names; asynchronous Isabelle_Process.init -- raw ML toplevel stays active; simplified Isabelle_Process using actors; misc tuning;
2010-08-08 wenzelm 2010-08-08 explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
2010-08-07 wenzelm 2010-08-07 simplified some Markup;
2010-08-07 wenzelm 2010-08-07 simplified type XML.Tree: embed Markup directly, avoid slightly odd triple; XML.cache_tree: actually store XML.Text as well; added Isabelle_Process.Result.properties;
2010-05-30 wenzelm 2010-05-30 separate markup for ML delimiters;
2010-05-30 wenzelm 2010-05-30 less pschedelic token markup;
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-05-25 wenzelm 2010-05-25 eliminated obsolete priority message from Isabelle_Process protocol;
2010-05-06 wenzelm 2010-05-06 replaced slightly odd fbreak markup by plain "\n", which also coincides with regular linebreaks produced outside the ML pretty engine;
2010-05-06 wenzelm 2010-05-06 basic support for symbolic pretty printing; tuned;
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-18 wenzelm 2009-12-18 markup bad YXML as malformed; removed unused XML.document; removed unused markup;
2009-12-10 wenzelm 2009-12-10 sealed XML.Tree; keep original XML.Tree within DOM as user data;
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-10-24 wenzelm 2009-10-24 markup for formal entities, with "def" or "ref" occurrences;
2009-08-29 wenzelm 2009-08-29 misc tuning;
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 added ML syntax markup;
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;
2008-12-29 wenzelm 2008-12-29 added POSITION_PROPERTIES;
2008-12-29 wenzelm 2008-12-29 more markup elements;
2008-12-28 wenzelm 2008-12-28 more markup elements;
2008-12-28 wenzelm 2008-12-28 more markup elements;
2008-12-19 wenzelm 2008-12-19 removed Ids;
2008-08-23 wenzelm 2008-08-23 added position, messages; renamed messages to content, malformed to bad;
2008-08-23 wenzelm 2008-08-23 Common markup elements.