Tue, 22 Apr 2014 12:05:02 +0200clarified exit code for the rare situation where Runtime.exn_error_message might fail;
wenzelm [Tue, 22 Apr 2014 12:05:02 +0200] rev 57972
clarified exit code for the rare situation where Runtime.exn_error_message might fail;

Tue, 22 Apr 2014 12:03:58 +0200tuned;
wenzelm [Tue, 22 Apr 2014 12:03:58 +0200] rev 57971
tuned;

Tue, 22 Apr 2014 11:53:05 +0200tuned -- avoid warning about catch-all handler;
wenzelm [Tue, 22 Apr 2014 11:53:05 +0200] rev 57970
tuned -- avoid warning about catch-all handler;

Tue, 22 Apr 2014 11:47:57 +0200more general exit;
wenzelm [Tue, 22 Apr 2014 11:47:57 +0200] rev 57969
more general exit;

Mon, 21 Apr 2014 21:16:05 +0200swap with qualifier;
haftmann [Mon, 21 Apr 2014 21:16:05 +0200] rev 57968
swap with qualifier;
tuned

Sun, 20 Apr 2014 00:25:05 +0100sos accepts False, returns apply command
paulson <lp15@cam.ac.uk> [Sun, 20 Apr 2014 00:25:05 +0100] rev 57967
sos accepts False, returns apply command

Sat, 19 Apr 2014 20:01:26 +0200clarified actor plumbing;
wenzelm [Sat, 19 Apr 2014 20:01:26 +0200] rev 57966
clarified actor plumbing;

Sat, 19 Apr 2014 19:52:02 +0200more elementary option sledgehammer_provers, avoiding complications of defaults from ML side (NB: guessing at number of cores does not make sense in PIDE);
wenzelm [Sat, 19 Apr 2014 19:52:02 +0200] rev 57965
more elementary option sledgehammer_provers, avoiding complications of defaults from ML side (NB: guessing at number of cores does not make sense in PIDE);

Sat, 19 Apr 2014 19:03:32 +0200clarified tooltip_lines: HTML.encode already takes care of newline (but not space);
wenzelm [Sat, 19 Apr 2014 19:03:32 +0200] rev 57964
clarified tooltip_lines: HTML.encode already takes care of newline (but not space);

Sat, 19 Apr 2014 18:37:41 +0200removed odd context argument: Thy_Info.get_theory does not fit into PIDE document model;
wenzelm [Sat, 19 Apr 2014 18:37:41 +0200] rev 57963
removed odd context argument: Thy_Info.get_theory does not fit into PIDE document model;