   (easy-menu-add specware-mode-menu)
   (if specware-use-x-symbol
       (x-symbol-mode t))
-  (if specware-use-hide-show
-      (hs-minor-mode t))
+  (when specware-use-hide-show
+    (hs-minor-mode t)
+    (setq hs-marker-begin-regexp "\\s-*%{{{")
+    (setq hs-marker-end-regexp "\\s-*%}}}"))
   (run-hooks 'specware-mode-hook))           ; Run the hook
 
 (defvar specware-mode-abbrev-table nil "*Specware mode abbrev table (default nil)")

		       (progn (beginning-of-line))
		     (end-of-buffer))
		   (forward-comment -100)) ; Go backward until non-comment found
	  (forward-sexp n))))))

(defun sw:adjust-begin (n)
  (point))


  (setq hs-minor-mode-map nil)		; Force resetting in case of old version
  (sw:load-specware-emacs-file "hideshow")
  (setq hs-allow-nesting t)
  (add-to-list 'hs-special-modes-alist
	       `(specware-mode ,(concat "\\(\\s(\\|\\s-*proof\\>\\|"
					sw:definition-intro-sexp
					"\\|"
					sw:basic-unit-intro-regexp
					"\\|%{{{"
					"\\)")
                               "\\(\\s)\\|\\<end-proof\\|\\<end-?spec\\|%}}}\\)"
			       nil
			       sw:forward-exp
			       sw:adjust-begin
			       )))

(defun sw:forward-exp (n)
