| Sat, 05 May 2018 22:33:35 +0200 |
wenzelm |
protocol message for export of theory resources;
|
file |
diff |
annotate
|
| Tue, 23 Jan 2018 19:25:39 +0100 |
wenzelm |
treat sessions as entities with defining position;
|
file |
diff |
annotate
|
| Fri, 19 Jan 2018 15:20:13 +0100 |
wenzelm |
sort completion result;
|
file |
diff |
annotate
|
| Fri, 19 Jan 2018 14:55:46 +0100 |
wenzelm |
formal treatment of documentation names;
|
file |
diff |
annotate
|
| Thu, 18 Jan 2018 21:41:30 +0100 |
wenzelm |
clarified access to antiquotation options;
|
file |
diff |
annotate
|
| Tue, 09 Jan 2018 15:40:12 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Sat, 16 Dec 2017 21:53:07 +0100 |
wenzelm |
added document antiquotation @{session name};
|
file |
diff |
annotate
|
| Sat, 16 Dec 2017 17:23:00 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 16 Dec 2017 16:46:01 +0100 |
wenzelm |
PIDE markup for session ROOT files;
|
file |
diff |
annotate
|
| Sat, 16 Dec 2017 15:15:51 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 16 Dec 2017 12:27:10 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Wed, 06 Dec 2017 18:59:33 +0100 |
wenzelm |
prefer control symbol antiquotations;
|
file |
diff |
annotate
|
| Tue, 28 Nov 2017 22:14:10 +0100 |
wenzelm |
clarified theory_name vs. loaded_theory: proper import_name for already loaded theories from other sessions (amending 4c98c929a12a);
|
file |
diff |
annotate
|
| Fri, 06 Oct 2017 21:14:00 +0200 |
wenzelm |
clarified error for bad session-qualified imports;
|
file |
diff |
annotate
|
| Thu, 28 Sep 2017 15:11:32 +0200 |
wenzelm |
session-qualified theory names are mandatory;
|
file |
diff |
annotate
|
| Thu, 28 Sep 2017 11:53:55 +0200 |
wenzelm |
discontinued extra checks (see ce676a750575 and 60c159d490a2) -- qualified theory names are meant to cover this;
|
file |
diff |
annotate
|
| Fri, 21 Apr 2017 14:09:03 +0200 |
wenzelm |
eliminated default_qualifier: just a constant;
|
file |
diff |
annotate
|
| Tue, 18 Apr 2017 16:34:58 +0200 |
wenzelm |
exclude theories from other sessions;
|
file |
diff |
annotate
|
| Tue, 18 Apr 2017 14:19:49 +0200 |
wenzelm |
actually qualify theory names;
|
file |
diff |
annotate
|
| Mon, 17 Apr 2017 20:33:18 +0200 |
wenzelm |
uniform use of theory base name for presentation;
|
file |
diff |
annotate
|
| Thu, 13 Apr 2017 12:39:36 +0200 |
wenzelm |
clarified init_session_base / finish_session_base: retain some information for plain "isabelle process", without rechecking dependencies as in "isabelle console";
|
file |
diff |
annotate
|
| Thu, 13 Apr 2017 12:19:28 +0200 |
wenzelm |
tuned signature (again);
|
file |
diff |
annotate
|
| Wed, 12 Apr 2017 23:35:42 +0200 |
wenzelm |
tuned according to Scala version;
|
file |
diff |
annotate
|
| Wed, 12 Apr 2017 22:32:55 +0200 |
wenzelm |
clarified loaded_theories: map to qualified theory name;
|
file |
diff |
annotate
|
| Mon, 10 Apr 2017 16:43:12 +0200 |
wenzelm |
proper import qualifier for global theories;
|
file |
diff |
annotate
|
| Mon, 10 Apr 2017 11:52:21 +0200 |
wenzelm |
clarified, according to Scala version;
|
file |
diff |
annotate
|
| Sat, 08 Apr 2017 22:36:32 +0200 |
wenzelm |
more qualifier treatment, but in the end it is still ignored;
|
file |
diff |
annotate
|
| Sat, 08 Apr 2017 21:28:19 +0200 |
wenzelm |
provide Resources.import_name in ML, similar to Scala version;
|
file |
diff |
annotate
|
| Sat, 08 Apr 2017 21:09:34 +0200 |
wenzelm |
clarified;
|
file |
diff |
annotate
|
| Sat, 08 Apr 2017 20:56:41 +0200 |
wenzelm |
more session_base information in ML;
|
file |
diff |
annotate
|
| Fri, 07 Apr 2017 21:06:48 +0200 |
wenzelm |
refer to known_theory;
|
file |
diff |
annotate
|
| Fri, 07 Apr 2017 19:35:39 +0200 |
wenzelm |
provide session base for "isabelle build" and "isabelle console" ML process;
|
file |
diff |
annotate
|
| Mon, 27 Feb 2017 16:29:52 +0100 |
wenzelm |
absent timing information means zero, according to 0070053570c4, f235646b1b73;
|
file |
diff |
annotate
|
| Fri, 12 Aug 2016 14:19:27 +0200 |
wenzelm |
uniform ML and document antiquotations;
|
file |
diff |
annotate
|
| Fri, 12 Aug 2016 13:34:59 +0200 |
wenzelm |
clarified error;
|
file |
diff |
annotate
|
| Thu, 11 Aug 2016 18:26:44 +0200 |
wenzelm |
clarified antiquotations;
|
file |
diff |
annotate
|
| Sat, 10 Oct 2015 16:21:34 +0200 |
wenzelm |
more explicit HTML.symbols;
|
file |
diff |
annotate
|
| Fri, 09 Oct 2015 21:16:00 +0200 |
wenzelm |
more direct HTML presentation, without print mode;
|
file |
diff |
annotate
|
| Mon, 16 Mar 2015 16:26:02 +0100 |
wenzelm |
tuned message -- include completion;
|
file |
diff |
annotate
|
| Fri, 13 Mar 2015 12:58:49 +0100 |
wenzelm |
simplified Command.resolve_files in ML, using blobs_index from Scala;
|
file |
diff |
annotate
|
| Tue, 09 Dec 2014 22:13:48 +0100 |
wenzelm |
imitate command markup and rendering of Isabelle/jEdit in HTML output;
|
file |
diff |
annotate
|
| Wed, 03 Dec 2014 14:04:38 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 07 Nov 2014 20:06:18 +0100 |
wenzelm |
prefer externally provided keywords -- Command.read_thy may degenerate to bootstrap_thy in case of errors;
|
file |
diff |
annotate
|
| Fri, 07 Nov 2014 16:36:55 +0100 |
wenzelm |
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
|
file |
diff |
annotate
|
| Thu, 06 Nov 2014 15:47:04 +0100 |
wenzelm |
more explicit Keyword.keywords;
|
file |
diff |
annotate
|
| Thu, 06 Nov 2014 11:44:41 +0100 |
wenzelm |
simplified keyword kinds;
|
file |
diff |
annotate
|
| Wed, 05 Nov 2014 20:49:30 +0100 |
wenzelm |
eliminated pointless dynamic keywords (TTY legacy);
|
file |
diff |
annotate
|
| Wed, 05 Nov 2014 20:20:57 +0100 |
wenzelm |
explicit type Keyword.keywords;
|
file |
diff |
annotate
|
| Sat, 01 Nov 2014 15:35:40 +0100 |
wenzelm |
tuned signature, in accordance to Scala version;
|
file |
diff |
annotate
|
| Fri, 31 Oct 2014 21:20:06 +0100 |
wenzelm |
obsolete;
|
file |
diff |
annotate
|
| Fri, 31 Oct 2014 18:56:59 +0100 |
wenzelm |
discontinued pointless option: timing is always on (overall theory only);
|
file |
diff |
annotate
|
| Tue, 21 Oct 2014 09:50:22 +0200 |
wenzelm |
clarified verbatim line breaks, e.g. relevant for Implementation mldecls;
|
file |
diff |
annotate
|
| Mon, 20 Oct 2014 16:52:36 +0200 |
wenzelm |
official support for "tt" style variants, avoid fragile \verb in LaTeX;
|
file |
diff |
annotate
|
| Tue, 12 Aug 2014 20:18:27 +0200 |
wenzelm |
tuned signature according to Scala version -- prefer explicit argument;
|
file |
diff |
annotate
|
| Tue, 12 Aug 2014 00:08:32 +0200 |
wenzelm |
separate module Command_Span: mostly syntactic representation;
|
file |
diff |
annotate
|
| Wed, 30 Apr 2014 22:45:26 +0200 |
wenzelm |
clarified signature: load_file is still required internally;
|
file |
diff |
annotate
|
| Mon, 31 Mar 2014 10:28:08 +0200 |
wenzelm |
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;
|
file |
diff |
annotate
|
| Wed, 26 Mar 2014 14:41:52 +0100 |
wenzelm |
prefer Context_Position where a context is available;
|
file |
diff |
annotate
|
| Wed, 26 Mar 2014 09:07:31 +0100 |
wenzelm |
superseded by (provide_)parse_files;
|
file |
diff |
annotate
|
| Tue, 18 Mar 2014 17:39:03 +0100 |
wenzelm |
clarifed module name;
|
file |
diff |
annotate
| base
|