diff options
Diffstat (limited to 'etc/isar/BackslashInStrings.thy')
-rw-r--r-- | etc/isar/BackslashInStrings.thy | 47 |
1 files changed, 47 insertions, 0 deletions
diff --git a/etc/isar/BackslashInStrings.thy b/etc/isar/BackslashInStrings.thy new file mode 100644 index 00000000..b1f91803 --- /dev/null +++ b/etc/isar/BackslashInStrings.thy @@ -0,0 +1,47 @@ +theory BackslashInStrings = Main: + +consts test :: string + +(* + +10.8.04 NB: Isar currently sets \ as word constituent ("w"). +Isabelle sets it as a punctuation element ("."). + +Experiments: (modify-syntax-entry ?\\ "w") + (modify-syntax-entry ?\\ ".") + +(add-hook 'isar-mode-hook + (lambda () (modify-syntax-entry ?\\ "\\"))) +*) + +defs test_def: "test == ''System.out.println(\"List from here:\")''" + + +end + + + +(* + +I'd be grateful for a little help in solving a bug/issue that I'm encountering in using Proof General with strings. It appears that Isar doesn't correctly understand Isabelle strings correctly. + +He's an example theory that throws up the observed issues: + +theory Test = Main: + +consts test :: string + +defs test_def: "test == ''System.out.println(\"List from here:\")''" + +end + +Firstly, anything between escaped double quotes is incorrectly highlighted. + +This is benign, unless an Isar keyword occurs between the double quotes (eg. from). In this case, Isabelle throws an error when it trys to parse the Isabelle term - mainly, it appears, because Isar/Proof General has passed Isabelle an incorrect term. + +I presume there's some Proof General regular expression that needs modifying here? + +Any help in fixing the issue is greatly appreciated. + +Thanks, +*) |