diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2008-07-05 16:47:14 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2008-07-05 16:47:14 +0000 |
| commit | c626065a6eabefd66e9a850dffe71a884cadafb3 (patch) | |
| tree | 57df5a4473eb04875e6754635b0a72f3993dfb0e /etc/trac | |
| parent | 619955d4b9949dd99a483fcf9daf8a4429301b82 (diff) | |
Trac regressions
Diffstat (limited to 'etc/trac')
| -rw-r--r-- | etc/trac/README | 1 | ||||
| -rw-r--r-- | etc/trac/trac-206.thy | 14 |
2 files changed, 15 insertions, 0 deletions
diff --git a/etc/trac/README b/etc/trac/README new file mode 100644 index 00000000..07b1721c --- /dev/null +++ b/etc/trac/README @@ -0,0 +1 @@ +Small tests for regressions. Indexed by trac bug number. diff --git a/etc/trac/trac-206.thy b/etc/trac/trac-206.thy new file mode 100644 index 00000000..d1d0a053 --- /dev/null +++ b/etc/trac/trac-206.thy @@ -0,0 +1,14 @@ +theory Test imports Main begin + +(* The special markup (for terms etc.) is not processed in minibuffer +messages. For example: *) + +ML_command {* warning (Syntax.string_of_typ @{context} @{typ 'a}) *} + +term "\<lambda> x. x" + +(* Here the decoration for 'a shows up as funny control characters, +instead of proper font-lock colouring. *) + +end + |