disabled auto resolve, until practical consequences are more clear;

example options;

proper platform_path;

clarified File.standard_path vs. File.platform_path (like Isabelle/Scala operations); avoid patching of SML basis library;

SOMEthing went wrong in eb87fc42825c;

include libgmp;

proper platform path for intial PolyML.SaveState.loadState; tuned signature;

proper platform path for initial load;

tuned signature;

keep native CInterface to make SHA1 work properly;

more setup for native Windows (Pure and HOL session with image);

basic setup for native Windows (RAW session without image);

more complete build;

support for native x86-windows via MinGW32;

no ML_debugger support in Pure -- too complicated;

more careful propagation of ML_debugger option to Pure;

support for ML files with/without debugger information;

explicit debug flag for ML compiler;

tuned;

abstract exn_id based on getExnId in polyml/basis/FinalPolyML.sml (NB: the mutable machine word cannot be inspected in ML, e.g. toplevel pp dumps core);

clarified initial ML name space (amending 7aad4be8a48e);

produce certified vars without access to theory_of_thm, and without context;

produce certified vars without access to theory_of_thm, and without context;

tuned;

added Thm.chyps_of; eliminated Thm.cprep_thm, with its potentially ill-typed (!) tpairs (cf. c9ad3e64ddcf);

prefer theory_id operations; tuned signature;

separate type theory_id;

delete precisely the added rules; tuned;

clarified context;

tuned whitespace;

tuned signature;

tuned;

tuned whitespace;

tuned whitespace;

obsolete;

clarified context;

clarified context;

tuned GUI;

proper setup of evaluation context;

tuned;

more robust access to stable tip version: take all pending edits into account, don't assume model for current buffer;

allow to break running threads at next possible breakpoint (simplified version of former option, see f3039309702e);

tuned signature;

qualified adjust_*

more lemmas

unfold intermediate definitions (stemming from composition) in lifted bnf operations

merged

more standard options; refrain from accessing PolyML internals;

prefer official @{make_string};

tuned signature, in accordance to sortBy in Scala;

clarified modules;

tuned NEWS

actually process lift_bnf regression suite

NEWS, CONTRIBUTORS, documentation for lift_bnf

use lift_bnf in an example

new command for lifting BNF structure over typedefs

more thorough reload;

resolve undefined blobs by default, e.g. relevant for ML debugger to avoid reset of breakpoints after reload;

merged

tuned colors;

clarified breakpoint rendering;

clarified;

default ML context for forks, e.g. relevant for debugging and toplevel pretty-printing;

clarified init/exit vs. session phase;

clarify type vs. term instantiation when forming closure;

more accurate dependencies;

tuned;

clarified thread re-selection;

clarified tree row handling;

proper context (amending 7aad4be8a48e);

suppress threads without debug state;

clarified events; tuned signature;

clarified GUI event handling;

tuned signature;

tuned;

misc tuning and clarification;

print values for stack entry;

clarified output;

default ML context for all command transactions, e.g. relevant for debugging and toplevel pretty-printing;

clarified break *point* position;

support hyperlinks with optional focus change; no change of focus for debuffer position, to avoid visual glitches and keep panel active;

tuned;

vacuous input means continue, e.g. after exit;

GUI actions depend on active debugger;

init/exit depending on active debugger panels;

eliminated cancel operation: disrupts normal evaluation of thread;

register thread such that cancel works;

clarified default selection;

report final debugger_state more robustly, e.g. after interrupt;

eliminated global option: breakpoints control this individually;

more uniform ScrollPane, like graphview;

tuned signature; more rendering;

tuned rendering;

set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;

more thorough Encode.string;

added action to toggle breakpoints (on editor side);