src/Pure/PIDE/command.ML
14 months ago wenzelm 2018-05-14 support for dynamic document output while editing;
14 months ago wenzelm 2018-05-09 clarified future scheduling parameters, with support for parallel_limit;
17 months ago wenzelm 2018-02-03 just one check of formal comments;
17 months ago wenzelm 2018-02-03 avoid proliferation of language_document reports; clarified signature;
17 months ago wenzelm 2018-01-28 clarified take/drop/chop prefix/suffix;
18 months ago wenzelm 2018-01-16 discontinued old form of marginal comments;
18 months ago wenzelm 2018-01-08 theory Pure is default presentation context;
18 months ago wenzelm 2018-01-08 check formal comments recursively, within arbitrary cartouches (unknown sublanguages);
19 months ago wenzelm 2017-12-13 positions as postlude: avoid intrusion of odd %-forms into main tex source;
19 months ago wenzelm 2017-12-12 simplified positions -- line is also human-readable in generated .tex file;
19 months ago wenzelm 2017-12-11 more robust range on preceding comment-line; no range for blank lines; avoid recursive output_text/mark_range; clarified Latex.output_token (no range) vs. Thy_Output.present_token (with range);
23 months ago wenzelm 2017-08-08 maintain "consolidated" status of theory nodes, which means all evals are finished (but not necessarily prints nor imports);
2017-06-22 wenzelm 2017-06-22 more informative task_statistics;
2017-05-27 wenzelm 2017-05-27 clarified build errors; tuned signature;
2016-12-28 wenzelm 2016-12-28 more uniform treatment of "bad" like other messages (with serial number);
2016-07-13 wenzelm 2016-07-13 obsolete;
2016-07-13 wenzelm 2016-07-13 semantic indentation for unstructured proof scripts;
2016-04-09 wenzelm 2016-04-09 tuned signature -- closer to Exn.Interrupt.expose in Scala;
2016-04-06 wenzelm 2016-04-06 treat ROOT.ML as theory with header "theory ML_Root imports ML_Bootstrap begin";
2016-04-02 wenzelm 2016-04-02 prefer infix operations;
2016-03-03 wenzelm 2016-03-03 clarified modules; tuned signature;
2015-10-16 wenzelm 2015-10-16 clarified Antiquote.antiq_reports; Thy_Output.output_text: support for markdown (inactive); eliminared Thy_Output.check_text -- uniform use of Thy_Output.output_text;
2015-10-09 wenzelm 2015-10-09 more direct HTML presentation, without print mode;
2015-09-21 wenzelm 2015-09-21 option editor_output_state;
2015-09-21 wenzelm 2015-09-21 separate panel for proof state output;
2015-06-29 wenzelm 2015-06-29 improved scheduling for urgent tasks, using farm of replacement threads (may lead to factor 2 overloading, but CPUs are usually hyperthreaded);
2015-04-16 wenzelm 2015-04-16 more explicit bootstrap_thy; clarified error;
2015-04-15 wenzelm 2015-04-15 tuned messages;
2015-04-12 wenzelm 2015-04-12 clarified language_path markup (again): exactly once *after* static phase, see also 83071f4c8ae6 and c043306d2598;
2015-04-07 wenzelm 2015-04-07 recovered additional Markup.language_path from c043306d2598, which is important to override Markup.string from Command.read phase, and thus ensure that symbol completion is disabled;
2015-03-25 wenzelm 2015-03-25 tuned signature;
2015-03-13 wenzelm 2015-03-13 simplified Command.resolve_files in ML, using blobs_index from Scala; clarified modules;
2015-03-12 wenzelm 2015-03-12 clarified markup for embedded files, early before execution;
2015-01-29 wenzelm 2015-01-29 discontinued special treatment of malformed commands (reverting e46cd0d26481), i.e. errors in outer syntax failure are treated like errors in inner syntax, name space lookup etc.;
2015-01-29 wenzelm 2015-01-29 ensure that running into older execution is interruptible (see also b91dc7ab3464);
2015-01-11 wenzelm 2015-01-11 do not crash into already running exec, instead join its lazy result in the subsequent step (amending 59f1591a11cb);
2015-01-09 wenzelm 2015-01-09 non-strict print_state: display old proof state on failure, e.g. unfinished command;
2015-01-09 wenzelm 2015-01-09 ignore print process even after fork, to avoid loosing active worker threads;
2014-12-28 wenzelm 2014-12-28 eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer); clarified Command.run_process etc.: join running eval, bypass running print; eliminated Command.memo in favour of regular Lazy.lazy; more Lazy.lazy status information;
2014-12-27 wenzelm 2014-12-27 memo_fork without locking, to avoid rare deadlock in Event_Timer.request due to execution overrun;
2014-12-09 wenzelm 2014-12-09 imitate command markup and rendering of Isabelle/jEdit in HTML output;
2014-11-26 wenzelm 2014-11-26 renamed "pairself" to "apply2", in accordance to @{apply 2};
2014-11-07 wenzelm 2014-11-07 prefer externally provided keywords -- Command.read_thy may degenerate to bootstrap_thy in case of errors; tuned message;
2014-11-07 wenzelm 2014-11-07 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes; plain value Outer_Syntax within theory: parsing requires current theory context; clarified name of Keyword.is_literal according to its semantics; eliminated pointless type Keyword.T; simplified @{command_spec}; clarified bootstrap keywords and syntax: take it as basis instead of side-branch;
2014-11-06 wenzelm 2014-11-06 more explicit Keyword.keywords;
2014-11-01 wenzelm 2014-11-01 tuned signature, in accordance to Scala version;
2014-10-31 wenzelm 2014-10-31 discontinued obsolete control command category;
2014-08-12 wenzelm 2014-08-12 separate module Command_Span: mostly syntactic representation; potentially prover-specific Output_Syntax.parse_spans;
2014-08-02 wenzelm 2014-08-02 more emphatic warning via error_message (violating historic TTY protocol);
2014-08-01 wenzelm 2014-08-01 prefer non-strict Execution.print, e.g relevant for redirected ML compiler reports after error (see also e79f76a48449 and 40274e4f5ebf);
2014-05-13 wenzelm 2014-05-13 no reset for 'end' -- e.g. relevant for 'notepad';
2014-05-12 wenzelm 2014-05-12 smarter recovery from toplevel type error;
2014-05-07 wenzelm 2014-05-07 run commands as interactive, again after long history of fluctuation (9e196062bf88, 173974e07dea, e07dacec79e7) and quite different infrastructure for print tasks;
2014-05-07 wenzelm 2014-05-07 discontinued Toplevel.print flag -- print uniformly according to Keyword.is_printed;
2014-05-06 wenzelm 2014-05-06 clarified print_state, which goes back to TTY loop before Proof General, and before separate print_context;
2014-05-06 wenzelm 2014-05-06 explicit option parallel_print to downgrade parallel scheduling, which might occasionally help for big and heavy "scripts";
2014-04-10 wenzelm 2014-04-10 tuned error -- allow user to click on hyperlink to open remote file;
2014-04-07 wenzelm 2014-04-07 simplified blob again (amending 1e77ed11f2f7): only store file node name, i.e. the raw editor file name; more liberal hyperlink to files, allow hyperlinks within editor files independently of the (POSIX) file-system;
2014-04-07 wenzelm 2014-04-07 separate file_node vs. file_path, e.g. relevant on Windows for hyperlink to the latter;
2014-03-31 wenzelm 2014-03-31 support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;