src/Pure/PIDE/command.ML
2014-03-10 wenzelm 2014-03-10 some Markup.language_path to prevent completion of symbols (notably "~") -- always "delimited" for simplicity in contrast to 42ac3cfb89f6;
2014-02-28 wenzelm 2014-02-28 tuned signature;
2014-02-27 wenzelm 2014-02-27 store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing; integrity check of SHA1 digests produced in Scala vs. ML; tuned signature;
2014-02-24 wenzelm 2014-02-24 clarified Token.range_of in accordance to Symbol_Pos.range; eliminated redundant Position.set_range, which is already included in Position.range;
2014-02-24 wenzelm 2014-02-24 tuned signature;
2014-02-11 wenzelm 2014-02-11 report (but ignore) markup within auxiliary files;
2013-12-05 wenzelm 2013-12-05 more uniform status -- accommodate spurious Exn.Interrupt from user code, allow ML_Compiler.exn_messages_id to crash; tuned signature;
2013-12-05 wenzelm 2013-12-05 merged, resolving obvious conflicts in NEWS and src/Pure/System/isabelle_process.ML;
2013-11-28 wenzelm 2013-11-28 more official task context via Task_Queue.enroll, which is required to participate in group cancellation (e.g. to terminate command exec); tuned signature;
2013-11-25 wenzelm 2013-11-25 more defensive order of Markup.failed vs. Markup.finished -- more informative status in Isabelle/Scala, although it is not rendered in Isabelle/jEdit;
2013-11-20 wenzelm 2013-11-20 register actual group of nested worker context -- relevant for insulated cancellation of exec_ids (see also 78693e46a237, e0169f13bd37); tuned signature;
2013-11-20 wenzelm 2013-11-20 proper static resolution of files via Thy_Load.load_thy, instead of TTY fall-back;
2013-11-20 wenzelm 2013-11-20 load files that are not provided by PIDE blobs; uniform resolve_files via Command.read;
2013-11-19 wenzelm 2013-11-19 more uniform handling of inlined files;
2013-11-19 wenzelm 2013-11-19 release file errors at runtime: Command.eval instead of Command.read;
2013-11-19 wenzelm 2013-11-19 maintain blobs within document state: digest + text in ML, digest-only in Scala; resolve files for command span, based on defined blobs; tuned;
2013-09-29 wenzelm 2013-09-29 low-priority print task is always asynchronous -- relevant for single-core machine and automatically tried tools;
2013-09-18 wenzelm 2013-09-18 improved printing of exception trace in Poly/ML 5.5.1;
2013-09-04 wenzelm 2013-09-04 non-persistent print_state: trade-off between JVM space vs. ML time;
2013-09-03 wenzelm 2013-09-03 Execution.fork formally requires registered Execution.running; Thy_Info.load_thy: more official exec_id registration (batch mode); dummy exec Document_ID.none is always registered (TTY mode); clarified exceptions for module Execution (NB: fork is used in user space, unlike protocol operations of Command and Document);
2013-08-25 wenzelm 2013-08-25 maintain goal forks as part of global execution; tuned;
2013-08-25 wenzelm 2013-08-25 discontinued parallel_subproofs_saturation and related internal counters (superseded by parallel_subproofs_threshold and timing information); simplified Goal.future_enabled;
2013-08-13 wenzelm 2013-08-13 more explicit error, e.g. for sledgehammer query operation applied in non-HOL session;
2013-08-10 wenzelm 2013-08-10 explicit "strict" flag for print functions (flipped internal meaning); non-strict query operations may operate on failed states;
2013-08-02 wenzelm 2013-08-02 prefer canonical order, to avoid potential fluctuation due to front-end edits;
2013-08-02 wenzelm 2013-08-02 support print functions with explicit arguments, as provided by overlays;
2013-07-30 wenzelm 2013-07-30 tuned;
2013-07-30 wenzelm 2013-07-30 de-assign execs that were not registered as running yet -- observe change of perspective more thoroughly;
2013-07-29 wenzelm 2013-07-29 keep memo_exec execution running, which is important to cancel goal forks eventually; run as nested worker task to keep main group valid, even after cancelation of removed subgroups; do not memoize interrupt, but absorb it silently in main execution; Goal.purge_futures: rough sanity check of group status;
2013-07-29 wenzelm 2013-07-29 maintain explicit execution frontier: avoid conflict with former task via static dependency; start execution immediate after assignment, to keep frontier simple;
2013-07-29 wenzelm 2013-07-29 clarified conditions for node traversal;
2013-07-29 wenzelm 2013-07-29 tuned signature;
2013-07-29 wenzelm 2013-07-29 discontinued notion of "stable" result -- running execution is never canceled;
2013-07-20 wenzelm 2013-07-20 print_state at high priority -- fast and important;
2013-07-15 wenzelm 2013-07-15 tuned;
2013-07-15 wenzelm 2013-07-15 keep persistent prints only if actually finished;
2013-07-13 wenzelm 2013-07-13 initial delay for automatically tried tools;
2013-07-13 wenzelm 2013-07-13 determine print function parameters dynamically, e.g. depending on runtime options;
2013-07-12 wenzelm 2013-07-12 reraise interrupts outside command regular transactions -- relevant for memo_stable;
2013-07-12 wenzelm 2013-07-12 clarified memo_exec: plain synchronized access without any special tricks;
2013-07-12 wenzelm 2013-07-12 clarified execution: maintain running execs only, check "stable" separately via memo (again); tuned signatures;
2013-07-12 wenzelm 2013-07-12 tuned signature; tuned comments;
2013-07-12 wenzelm 2013-07-12 clarified module name;
2013-07-11 wenzelm 2013-07-11 more explicit type Exec.context; eliminated obsolete execution group -- NB: cancelation happens individually for registered execs;
2013-07-11 wenzelm 2013-07-11 strictly monotonic Document.update: avoid disruptive cancel_execution, merely discontinue_execution and cancel/terminate old execs individually;
2013-07-11 wenzelm 2013-07-11 more abstract types; tuned signature;
2013-07-11 wenzelm 2013-07-11 disallow concurrent execution attempt explicitly -- it should never happen due to management of singleton execution; tuned error messages: prefer plain "error" as in document.ML;
2013-07-11 wenzelm 2013-07-11 global management of command execution fragments; tuned;
2013-07-11 wenzelm 2013-07-11 tuned;
2013-07-10 wenzelm 2013-07-10 print "persistent" flag allows to adjust tradeoff of ML run-time vs. JVM heap-space;
2013-07-10 wenzelm 2013-07-10 allow to remove print functions; tuned signature;
2013-07-10 wenzelm 2013-07-10 clarified Command.print: update old prints here;
2013-07-09 wenzelm 2013-07-09 more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
2013-07-08 wenzelm 2013-07-08 more direct interleaving of eval/print and update/execution -- refrain from crude manipulation of max_threads;
2013-07-05 wenzelm 2013-07-05 tuned signature; tuned comments;
2013-07-05 wenzelm 2013-07-05 tuned signature -- eliminated pointless type synonym;
2013-07-05 wenzelm 2013-07-05 tuned signature; tuned;
2013-07-05 wenzelm 2013-07-05 clarified type Command.eval;
2013-07-05 wenzelm 2013-07-05 tuned signature;
2013-07-05 wenzelm 2013-07-05 explicit module Document_ID as source of globally unique identifiers across ML/Scala;