New files.

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,
+*)