| Thu, 15 Mar 2012 10:16:21 +0100 |
explicit Outer_Syntax.Decl;
|
file | diff | annotate |
| Thu, 15 Mar 2012 09:55:42 +0100 |
allow multiple 'keywords' as in 'fixes';
|
file | diff | annotate |
| Thu, 15 Mar 2012 00:10:45 +0100 |
some support for outer syntax keyword declarations within theory header;
|
file | diff | annotate |
| Wed, 29 Feb 2012 23:09:06 +0100 |
clarified module Thy_Load;
|
file | diff | annotate |
| Sun, 26 Feb 2012 15:18:48 +0100 |
tuned signature;
|
file | diff | annotate |
| Tue, 30 Aug 2011 12:01:07 +0200 |
do not normalized extra file dependencies for now -- still loaded by prover process;
|
file | diff | annotate |
| Tue, 16 Aug 2011 22:48:31 +0200 |
more robust Thy_Header.base_name, with minimal assumptions about path syntax;
|
file | diff | annotate |
| Tue, 16 Aug 2011 21:13:52 +0200 |
use full .thy file name as node name, which makes MiscUtilities.resolveSymlinks/File.getCanonicalPath more predictable;
|
file | diff | annotate |
| Sat, 13 Aug 2011 20:20:36 +0200 |
provide node header via Scala layer;
|
file | diff | annotate |
| Fri, 12 Aug 2011 22:10:49 +0200 |
normalized theory dependencies wrt. file_store;
|
file | diff | annotate |
| Fri, 12 Aug 2011 15:28:30 +0200 |
clarified document model header: master_dir (native wrt. editor, potentially URL) and node_name (full canonical path);
|
file | diff | annotate |
| Fri, 12 Aug 2011 12:03:17 +0200 |
simplified class Thy_Header;
|
file | diff | annotate |
| Thu, 11 Aug 2011 20:32:44 +0200 |
uniform treatment of header edits as document edits;
|
file | diff | annotate |
| Tue, 12 Jul 2011 10:44:30 +0200 |
tuned XML modules;
|
file | diff | annotate |
| Sun, 10 Jul 2011 20:59:04 +0200 |
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
|
file | diff | annotate |
| Sun, 10 Jul 2011 15:48:15 +0200 |
more abstract signature;
|
file | diff | annotate |
| Sun, 10 Jul 2011 13:51:21 +0200 |
simplified XML_Data;
|
file | diff | annotate |
| Sun, 10 Jul 2011 13:00:22 +0200 |
less currying in Scala;
|
file | diff | annotate |
| Sun, 10 Jul 2011 00:21:19 +0200 |
propagate header changes to prover process;
|
file | diff | annotate |
| Fri, 08 Jul 2011 11:13:21 +0200 |
tuned signature;
|
file | diff | annotate |
| Thu, 07 Jul 2011 22:04:30 +0200 |
explicit Document.Node.Header, with master_dir and thy_name;
|
file | diff | annotate |
| Thu, 07 Jul 2011 13:48:30 +0200 |
simplified Symbol based on lazy Symbol.Interpretation -- reduced odd "functorial style";
|
file | diff | annotate |
| Tue, 05 Jul 2011 22:38:44 +0200 |
theory name needs to conform to Path syntax;
|
file | diff | annotate |
| Mon, 04 Jul 2011 22:11:32 +0200 |
quasi-static Isabelle_System -- reduced tendency towards "functorial style";
|
file | diff | annotate |
| Mon, 04 Jul 2011 16:51:45 +0200 |
pervasive Basic_Library in Scala;
|
file | diff | annotate |
| Sun, 03 Jul 2011 19:42:32 +0200 |
more explicit edit_node vs. init_node;
|
file | diff | annotate |
| Sat, 02 Jul 2011 23:31:07 +0200 |
Thy_Header.read convenience;
|
file | diff | annotate |
| Thu, 30 Jun 2011 19:24:09 +0200 |
more general theory header parsing;
|
file | diff | annotate |
| Thu, 13 Jan 2011 17:30:52 +0100 |
clarified split_thy_path;
|
file | diff | annotate |
| Thu, 23 Sep 2010 18:44:26 +0200 |
explicit Session.Phase indication with associated event bus;
|
file | diff | annotate |
| Thu, 05 Aug 2010 13:41:00 +0200 |
somewhat uniform Thy_Header.split_thy_path in ML and Scala;
|
file | diff | annotate |
| Mon, 17 May 2010 14:23:54 +0200 |
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
|
file | diff | annotate |
| Sat, 15 May 2010 22:15:57 +0200 |
renamed Outer_Parse to Parse (in Scala);
|
file | diff | annotate |
| Sat, 09 Jan 2010 23:22:56 +0100 |
misc tuning;
|
file | diff | annotate |
| Mon, 28 Dec 2009 22:03:14 +0100 |
separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
|
file | diff | annotate |
| Mon, 28 Dec 2009 18:40:13 +0100 |
moved Library.decode_permissive_utf8 to Isabelle_System;
|
file | diff | annotate |
| Sun, 27 Dec 2009 23:10:03 +0100 |
allow UTF-8 in theory and file names;
|
file | diff | annotate |
| Sun, 27 Dec 2009 22:36:47 +0100 |
read header by scanning/parsing file;
|
file | diff | annotate |
| Sun, 27 Dec 2009 21:34:23 +0100 |
scan: operate on file (via Scan.byte_reader), more robust exception handling;
|
file | diff | annotate |
| Tue, 22 Dec 2009 21:48:17 +0100 |
basic setup for header scanning/parsing;
|
file | diff | annotate |
| Tue, 01 Sep 2009 14:45:06 +0200 |
modernized Thy_Header;
|
file | diff | annotate |
| Sat, 29 Aug 2009 14:31:39 +0200 |
misc tuning;
|
file | diff | annotate |
| Fri, 19 Dec 2008 20:37:29 +0100 |
removed Ids;
|
file | diff | annotate |
| Sat, 04 Oct 2008 14:29:42 +0200 |
Theory header keywords.
|
file | diff | annotate |