diff options
| author | Makarius Wenzel | 2000-06-04 12:37:17 +0000 |
|---|---|---|
| committer | Makarius Wenzel | 2000-06-04 12:37:17 +0000 |
| commit | 177a4fdf3ef6fe51c1721595088d0e779da26991 (patch) | |
| tree | ffb9d8dadb3ecca354e6040978b817d3b021a091 | |
| parent | 87e6f0630d21ff06a902cac8de98e942fab274dc (diff) | |
replaced isar-verbatim by isabelle-verbatim;
fixed output syntax table;
| -rw-r--r-- | isar/isar-syntax.el | 13 |
1 files changed, 6 insertions, 7 deletions
diff --git a/isar/isar-syntax.el b/isar/isar-syntax.el index bf6acd49..a14ae6de 100644 --- a/isar/isar-syntax.el +++ b/isar/isar-syntax.el @@ -60,7 +60,12 @@ (isar-init-syntax-table) ;; ignore strings so font-locking works ;; inside them - (modify-syntax-entry ?\" " ")) + (modify-syntax-entry ?\" " ") + (modify-syntax-entry ?\* ".") + (modify-syntax-entry ?\( "()") + (modify-syntax-entry ?\) ")(") + (modify-syntax-entry ?\{ "(}") + (modify-syntax-entry ?\} "){")) ;; ----- syntax for font-lock and other features @@ -182,12 +187,6 @@ (concat "\\(" (isar-ids-to-regexp isar-keywords-theory-goal) "\\)" isar-name-regexp ":") "Regexp matching goal commands in Isabelle/Isar which name a theorem") -(defconst isar-verbatim-regexp "^\^VERBATIM: \\(\\(.\\|\n\\)*\\)$" - "Regexp matching internal marker for verbatim command output") - -(defun isar-verbatim (str) - "Mark internal command for verbatim output" - (concat "\^VERBATIM: " str)) ;; ----- Isabelle inner syntax hilite |