From cd9ded92db606021620089b492737d1f32a3fcdd Mon Sep 17 00:00:00 2001 From: malc Date: Mon, 10 Aug 2015 01:47:36 +0300 Subject: [PATCH] Fix reentering narrowed outline Breakage due to 3b82ef35665ef956bf6d80d3af1ad63ceff827bf. Mutability strikes again. --- main.ml | 17 +++++++++++++---- 1 file changed, 13 insertions(+), 4 deletions(-) diff --git a/main.ml b/main.ml index f086c31..95dce31 100644 --- a/main.ml +++ b/main.ml @@ -4690,11 +4690,20 @@ let enterselector sourcetype = ) ;; -let enteroutlinemode () = enterselector `outlines "Document has no outline";; -let enterbookmarkmode () = - enterselector `bookmarks "Document has no bookmarks (yet)" +let enteroutlinemode = + let f = enterselector `outlines in + fun () -> f "Document has no outline" +;; + +let enterbookmarkmode = + let f = enterselector `bookmarks in + fun () -> f "Document has no bookmarks (yet)" +;; + +let enterhistmode = + let f = enterselector `history in + fun () -> f "No history (yet)" ;; -let enterhistmode () = enterselector `history "No history (yet)";; let quickbookmark ?title () = match state.layout with -- 2.11.4.GIT