Attempt to duplicate Dixon bug

2 files changed, 26 insertions, 0 deletions

diff --git a/etc/isar/BigErrors.thy b/etc/isar/BigErrors.thy
new file mode 100644
index 00000000..803fdf29
--- /dev/null
+++ b/etc/isar/BigErrors.thy
@@ -0,0 +1,20 @@
+(* See http://proofgeneral.inf.ed.ac.uk/trac/ticket/274 *)
+
+theory BigErrors imports Pure 
+begin
+
+consts foo :: 'a;
+consts bar :: 'a;
+
+ML {* warning (cat_lines (List.tabulate (300,K "This is a big warning message"))); *}
+
+(* Attempt to get a big error with "error" fails, but we can use printing function
+   (see FaultyErrors.thy) *)
+
+ML {* Output.error_msg (cat_lines (List.tabulate (10000,K "This is a big error message"))); *}
+
+(* Note about FaultyErrors: the above generates an error
+   interactively but does *not* generate an error when 
+   required by another theory, see, BigErrorsNested *)
+
+end;
diff --git a/etc/isar/BigErrorsNested.thy b/etc/isar/BigErrorsNested.thy
new file mode 100644
index 00000000..69fa7142
--- /dev/null
+++ b/etc/isar/BigErrorsNested.thy
@@ -0,0 +1,6 @@
+(* See http://proofgeneral.inf.ed.ac.uk/trac/ticket/274 *)
+
+theory BigErrorsNested imports BigErrors 
+begin
+
+end