# HG changeset patch
# User wenzelm
# Date 927830850 -7200
# Node ID 5d50225637c8b01c5095f68ec406f09ab0e55e58
# Parent  6b5cb872d9975e3619aff009caf556bd06061b58
changed {| |} verbatim syntax to {* *} in order to simplify ProofGeneral setup;

diff -r 6b5cb872d997 -r 5d50225637c8 src/Pure/Isar/outer_lex.ML
--- a/src/Pure/Isar/outer_lex.ML	Thu May 27 20:45:20 1999 +0200
+++ b/src/Pure/Isar/outer_lex.ML	Thu May 27 20:47:30 1999 +0200
@@ -144,13 +144,13 @@
 
 val scan_verb =
   scan_blank ||
-  keep_line ($$ "|" --| Scan.ahead (Scan.one (not_equal "}"))) ||
-  keep_line (Scan.one (not_equal "|" andf Symbol.not_eof));
+  keep_line ($$ "*" --| Scan.ahead (Scan.one (not_equal "}"))) ||
+  keep_line (Scan.one (not_equal "*" andf Symbol.not_eof));
 
 val scan_verbatim =
-  keep_line ($$ "{" -- $$ "|") |--
+  keep_line ($$ "{" -- $$ "*") |--
     !! (lex_err (K "missing end of verbatim text"))
-      (change_prompt ((Scan.repeat scan_verb >> implode) --| keep_line ($$ "|" -- $$ "}")));
+      (change_prompt ((Scan.repeat scan_verb >> implode) --| keep_line ($$ "*" -- $$ "}")));
 
 
 (* scan space *)