more robust system channel via options that are private to the user;

support Store with options;

clarified signature;

tuned signature;

avoid println with its extra CR on Windows;

tuned signature;

clarified signature: tree structure is not essential;

clarified YXML vs. symbol encoding: operate on whole message;
tuned signature;

simplified signature (despite 448325de6e4f);

more process arguments;

support for permanent phase_changed watcher;

more explicit Session.xml_cache;

tuned signature;

proper session dirs for "isabelle jedit" and "isabelle console" with options -d and -l;

discontinued slightly odd "secure" mode;

less physical "logic" argument, with option -l like "isabelle console" etc.;

find heaps uniformly via Sessions.Store;
tuned;

clarified modules;

--HG--
rename : src/Pure/System/ml_process.scala => src/Pure/Tools/ml_process.scala

tuned signature;

more abstract Session.start, without prover command-line;
Isabelle_Process.apply is directly based on ML_Process;
clarified Isabelle_Process.main command-line;
tuned signature;

removed pointless option: this is meant for web services using Isabelle/Scala, not command-line tools;

prospective command line entry point for simplified isabelle_process;

clarified treatment of DEL;
tuned signature;

Bash.process always uses a closed script instead of an open argument list, for extra robustness on Windows, where quoting is not well-defined;
more robust File.bash_escape;
more robust treatment of ML_OPTIONS;
clarified prover args (again);

tuned whitespace;

more careful quoting for the sake of Windows;

tuned signature;

clarified bash process -- similar to ML version;

clarified modules, like ML version;

misc tuning, based on warnings by IntelliJ IDEA;

tuned signature;

generic process wrapping in Prover;
clarified module arrangement;

more abstract Prover.System_Process, which allows to bypass Isabelle_System.Managed_Process;

prefer scala.Console with its support for thread-local redirection;

clarified exit sequence: prover is reset afterwards, no more output messages;

clarified;

tuned comments;

tuned imports;

clarified command_input: Consumer_Thread;

eliminated pointless output actors;
clarified command_input, which already includes thread.join;

reintroduced process interrupt for the sake of synchronous protocol commands like "use_theories" (see also 27930cf6f0f7);

recovered public command_line from d92eb5c3960d, which is important for alternative prover processes;

more general prover operations;

more general prover operations;

tuned imports;

more distinctive Isabelle_Process.Output vs. Isabelle_Process.Protocol_Output;

more specific Protocol_Output: empty message.body, main content via bytes/text;

tuned signature;

tuned signature -- facilitate experimentation with other processes;

tuned -- more uniform ML vs. Scala;

tuned signature;

no need for raw stdin;

public Isabelle_Process.xml_cache (thread-safe);
cache derived status messages;

tuned signature;

explicit module UTF8;

Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;

update options via protocol;
jEdit dialog for "Parallel Checking" options;

more direct message header: eliminated historic encoding via single letter;

earlier treatment of embedded report/no_report messages (see also 4110cc1b8f9f);

tuned signature -- slightly more abstract text representation of prover process;

support for detached Bash_Job with some control operations;

support external processes with explicit environment;

clarified prover startup: no timeout, read stderr more carefully;

need to close_input before expecting threads to terminate/join;
tuned signature;

more explicit treatment of return code vs. session phase;

clarified terminology of raw protocol messages;

tuned;

tuned signature -- emphasize Isabelle_Process Input vs. Output;

clarified scope of exception handlers;

terminate after first exception -- avoid syslog flooding;

clarified initial process startup errors: recover image load failure message (cf. 2cb7e34f6096) and suppress accidental output from raw ML toplevel;

prefer raw_message for protocol implementation;

clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;

--HG--
rename : src/Pure/PIDE/isabelle_document.ML => src/Pure/PIDE/protocol.ML
rename : src/Pure/PIDE/isabelle_document.scala => src/Pure/PIDE/protocol.scala

clarified modules;

--HG--
rename : src/Pure/PIDE/isar_document.ML => src/Pure/PIDE/isabelle_document.ML
rename : src/Pure/PIDE/isar_document.scala => src/Pure/PIDE/isabelle_document.scala

separate module for concrete Isabelle markup;

--HG--
rename : src/Pure/General/markup.ML => src/Pure/General/isabelle_markup.ML
rename : src/Pure/General/markup.scala => src/Pure/General/isabelle_markup.scala

retain stderr and include it in syslog, which is buffered and thus increases the chance that users see remains from crashes etc.;

always use sockets on Windows/Cygwin;
discontinued special raw_dump facility;

more uniform defaults;

explicit option for socket vs. fifo communication;

more abstract wrapping of fifos as System_Channel;

added "cancel" button based on cancel_execution, not interrupt (cf. 156be0e43336);

buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;

more abstract receiver interface;

simplified signatures;

pass raw messages through xml_cache actor, which is important to retain ordering of results (e.g. read_command reports before assign, cf. 383c9d758a56);

more uniform Properties in ML and Scala;

JVM method invocation service via Scala layer;

tuned signature;

some support for raw messages, which bypass standard Symbol/YXML decoding;
tuned signature;

tuned XML.Cache parameters;

echo prover input via raw_messages, for improved protocol tracing;

simplified Symbol based on lazy Symbol.Interpretation -- reduced odd "functorial style";
tuned implicit build/init messages;

quasi-static Isabelle_System -- reduced tendency towards "functorial style";

explicit import java.lang.System to prevent odd scope problems;

lazy Isabelle_System.default supports implicit boot;

updated headers;

more abstract/uniform handling of time, preferring seconds as Double;

bulk read: observe EOF protocol more carefully -- 0 counts as successful read;

tuned messages -- cf. Admin/MacOS/App1;

explicit Session.Phase indication with associated event bus;
asynchronous Session.start();
synchronous Session.stop();
added Plugin.session_manager on top of basic Session;
eliminated separate isabelle.activate action;
misc tuning;

manage persistent syslog via Session, not Isabelle_Process;
tuned;

tuned prover message categorization;

tuned message;

tuned message;

more content for Session_Dockable;

more reactive handling of Isabelle_Process startup errors;

main Isabelle_Process via Isabelle_System.Managed_Process;
simplified init message: no pid;
misc tuning and simplification;

tuned;

tuned;

added Isabelle_Process.syslog;
refined Isabelle_Process.process_manager: startup_output via syslog, explicit join of auxiliary threads;
tuned;

Isabelle_Process: more robust rendezvous, even without proper blocking on open (Cygwin);

refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
tuned;

message_actor: more robust treatment of EOF;

simplified Isabelle_Process message kinds;
misc tuning and simplification;

recovered basic session stop/restart;

simplified fifo handling -- rm_fifo always succeeds without ever blocking;
tuned;

slightly more robust Isabelle_Process startup -- NB: openening fifo streams synchronizes with other end, which may fail to reach that point;

discontinued Output.debug, which belongs to early PGIP experiments (b6788dbd2ef9) and causes just too many problems (like spamming the message channel if it is used by more than one module);

eliminated markup "location" in favour of more explicit "no_report", which is actually deleted from messages;

module for simplified thread operations (Scala version);

tuned signatures;

XML.Cache: pipe-lined (thread-safe) version using actor;
tuned Isabelle_Process.pid handling;

simplified internal message format: dropped special Symbol.STX header;

added Isabelle_Process.input_bytes, which avoids the somewhat slow Standard_System.string_bytes (just in case someone wants to stream raw data at 250MB/s);

native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
misc clarification of proc/pid state, eliminated closing flag;
misc tuning and simplification;

removed obsolete methods for (ML) commands;

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;

Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
some partial workarounds for Cygwin;

explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);

simplified some Markup;

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;

specific ML_val vs. ML_command;

simplified Isabelle_Process.Result: use markup directly;

indicate prospective properties;

eliminated obsolete priority message from Isabelle_Process protocol;

simplified message markup, using plain XML.Elem directly;

more abstract view on prover output messages;

output symbolic pretty printing markup and format in the front end;

added is_ready;

simplified init message -- removed redundant session property;

removed obsolete version check -- sanity delegated to Isabelle_System;
tuned;

separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);

tuned signature;

Result.cache;

fifo: raw byte stream;
Result: fully decoded symbols and tree structure;
adapted to simplified message format;
tuned;

Isabelle_Process: receiver as Actor, not EventBus;
removed misleading Isabelle_Process.parse_message method -- use plain function instead;

moved Pure/Tools/isabelle_syntax.scala to Pure/System/isabelle_syntax.scala;
renamed object IsabelleSyntax to Isabelle_Syntax;

--HG--
rename : src/Pure/Tools/isabelle_syntax.scala => src/Pure/System/isabelle_syntax.scala

renamed IsabelleProcess to Isabelle_Process;
renamed IsabelleSystem to Isabelle_System;

static IsabelleSystem.charset;
static IsabelleSystem.is_cygwin -- based on system property "os.name";
smart bootstrapping of Isabelle settings environment (via implicit or explicit ISABELLE_TOOL, or isabelle.tool property, or isabelle via PATH);
source_file: removed obsolete special treatment of "ML";
misc tuning and reorganization;

moved isabelle_process.ML, isabelle_process.scala, isar.ML, session.ML to Pure/System/ (together with associated Isar commands);

--HG--
rename : src/Pure/Tools/isabelle_process.ML => src/Pure/System/isabelle_process.ML
rename : src/Pure/Tools/isabelle_process.scala => src/Pure/System/isabelle_process.scala
rename : src/Pure/Isar/isar.ML => src/Pure/System/isar.ML
rename : src/Pure/Isar/session.ML => src/Pure/System/session.ML