src/Pure/Thy/thy_load.scala
Mon, 03 Mar 2014 11:58:07 +0100 wenzelm clarified path checks: avoid crash of rendering due to spurious errors;
Sat, 25 Jan 2014 15:29:40 +0100 wenzelm propagate update of outer syntax keywords: global propertiesChanged, buffer TokenMarker.markTokens, text area repainting;
Tue, 19 Nov 2013 20:53:43 +0100 wenzelm clarified Document.Blobs environment vs. actual edits of auxiliary files;
Tue, 19 Nov 2013 19:33:27 +0100 wenzelm maintain blobs within document state: digest + text in ML, digest-only in Scala;
Tue, 19 Nov 2013 13:39:12 +0100 wenzelm proper Thy_Load.append of auxiliary file names;
Tue, 19 Nov 2013 12:57:56 +0100 wenzelm clarified boundary cases of Document.Node.Name;
Mon, 18 Nov 2013 23:46:59 +0100 wenzelm clarified Thy_Load.node_name;
Mon, 18 Nov 2013 23:26:15 +0100 wenzelm inline blobs into command, via SHA1 digest;
Mon, 08 Apr 2013 14:18:39 +0200 wenzelm more general Thy_Load.import_name, e.g. relevant for Isabelle/eclipse -- NB: Thy_Load serves as main hub for funny overriding to adapt to provers and editors;
Wed, 27 Feb 2013 12:45:19 +0100 wenzelm discontinued obsolete 'uses' within theory header;
Sun, 30 Dec 2012 18:23:31 +0100 wenzelm tuned;
Sun, 16 Dec 2012 18:44:27 +0100 wenzelm tuned signature: use thy_load to adapt to prover/editor specific view on sources;
Fri, 07 Dec 2012 13:56:01 +0100 wenzelm fork slow part of Thy_Load.body_files only;
Fri, 07 Dec 2012 13:38:32 +0100 wenzelm explore theory_body_files via future, for improved performance;
Fri, 30 Nov 2012 10:42:54 +0100 wenzelm prefer Symbol.decode_strict in batch mode, to avoid files with spurious Unicode symbols that clash with Isabelle symbol interpretation;
Sun, 25 Nov 2012 20:31:49 +0100 wenzelm tuned signature -- avoid intrusion of module Path in generic PIDE concepts;
Wed, 22 Aug 2012 21:43:17 +0200 wenzelm add keywords of this node as well (e.g. relevant for Pure.thy);
Wed, 22 Aug 2012 18:04:30 +0200 wenzelm find files via load commands within theory text;
Wed, 22 Aug 2012 16:10:23 +0200 wenzelm pass syntax through check_thy;
Wed, 22 Aug 2012 15:53:17 +0200 wenzelm use Thy_Header.read on explicit text only -- potentially via File.read, not Scan.byte_reader;
Tue, 21 Aug 2012 12:15:25 +0200 wenzelm clarified initialization of Thy_Load, Thy_Info, Session;
Thu, 16 Aug 2012 15:40:26 +0200 wenzelm more robust multi-platform support;
Tue, 07 Aug 2012 17:46:30 +0200 wenzelm need to expand path in order to resolve imports like "~~/src/Tools/Code_Generator";
Tue, 07 Aug 2012 17:08:22 +0200 wenzelm prefer static Build.session_content for loaded theories -- discontinued incremental protocol;
Tue, 07 Aug 2012 15:01:48 +0200 wenzelm simplified Document.Node.Header -- internalized errors;
Tue, 24 Jul 2012 20:56:18 +0200 wenzelm more explicit checks during parsing;
Sun, 22 Jul 2012 00:00:22 +0200 wenzelm determine source dependencies, relatively to preloaded theories;
Fri, 20 Jul 2012 22:29:25 +0200 wenzelm more explicit java.io.{File => JFile};
Thu, 15 Mar 2012 00:10:45 +0100 wenzelm some support for outer syntax keyword declarations within theory header;
Sat, 03 Mar 2012 14:04:49 +0100 wenzelm retain original "uses" (again) -- still required for Thy_Load.use_file etc. in ML (notably for maintaining required/provided);
Thu, 01 Mar 2012 15:16:20 +0100 wenzelm refined node_header -- more direct buffer access (again);
Wed, 29 Feb 2012 23:09:06 +0100 wenzelm clarified module Thy_Load;
Sat, 17 Sep 2011 17:55:39 +0200 wenzelm sane default for class Thy_Load;
Thu, 01 Sep 2011 13:39:40 +0200 wenzelm tuned signature;
Thu, 01 Sep 2011 13:34:45 +0200 wenzelm more abstract Document.Node.Name;
Tue, 30 Aug 2011 11:43:47 +0200 wenzelm separate module for jEdit primitives for loading theory files;
Mon, 29 Aug 2011 21:55:49 +0200 wenzelm actual auto loading of required files;
Fri, 12 Aug 2011 12:03:17 +0200 wenzelm simplified class Thy_Header;
Tue, 05 Jul 2011 22:39:15 +0200 wenzelm Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;
Mon, 04 Jul 2011 16:27:11 +0200 wenzelm some support for theory files within Isabelle/Scala session;
less more (0) tip