aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/nanoPG.ml
blob: 805ace935c4a2133a21378d1a443201addb586e2 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

open Ideutils
open Session
open Preferences
open GdkKeysyms
open Printf

let eprintf x =
  if !Flags.debug then Printf.eprintf x else Printf.ifprintf stderr x

type gui = {
  notebook : session Wg_Notebook.typed_notebook;
  action_groups : GAction.action_group list;
}

let actiong gui name = List.find (fun ag -> ag#name = name) gui.action_groups
let ct gui = gui.notebook#current_term

let get_sel b = b#selection_bounds
let sel_nonempty b = let i, j = get_sel b in not (i#equal j)
let get_sel_txt b = let i, j = get_sel b in i#get_text ~stop:j

type status = { move : int option; kill : (string * bool) option; sel: bool }

let pr_status { move; kill; sel } =
  let move = Option.cata (fun i -> string_of_int i) "" move in
  let kill = Option.cata (fun (s,b) -> sprintf "kill(%b) %S" b s) "" kill in
  let sel = string_of_bool sel in
  Printf.sprintf "{ move: %s; kill: %s; sel: %s }" move kill sel
let pr_key t =
  let kv = GdkEvent.Key.keyval t in
  let str = GdkEvent.Key.string t in
  let str_of_mod = function
  | `SHIFT -> "SHIFT" | `LOCK -> "LOCK" | `CONTROL -> "CONTROL"
  | `MOD1 -> "MOD1" | `MOD2 -> "MOD2" | `MOD3 -> "MOD3" | `MOD4 -> "MOD4"
  | `MOD5 -> "MOD5" | `BUTTON1 -> "BUTTON1" | `BUTTON2 -> "BUTTON2"
  | `BUTTON3 -> "BUTTON3" | `BUTTON4 -> "BUTTON4" | `BUTTON5 -> "BUTTON5"
  | `SUPER -> "SUPER" | `HYPER -> "HYPER" | `META -> "META"
  | `RELEASE -> "RELEASE" in
  let mods = String.concat " " (List.map str_of_mod (GdkEvent.Key.state t)) in
  Printf.sprintf "'%s' (%d, %s)" str kv mods

type action =
  | Action of string * string
  | Callback of (gui -> unit)
  | Edit of (status -> GSourceView2.source_buffer -> GText.iter ->
              (string -> string -> unit) -> status)
  | Motion of (status -> GText.iter -> GText.iter * status)

type 'c entry = {
  mods : Gdk.Tags.modifier list;
  key : Gdk.keysym;
  keyname : string;
  doc : string;
  contents : 'c
}

let mC = [`CONTROL]
let mM = [`MOD1]

let mod_of t x = List.for_all (fun m -> List.mem m (GdkEvent.Key.state t)) x

let pr_keymod l =
  if l = mC then "C-"
  else if l = mM then "M-"
  else ""

let mkE ?(mods=mC) key keyname doc ?(alias=[]) contents =
  List.map (fun (mods, key, keyname) -> { mods; key; keyname; doc; contents })
    ((mods, key, keyname)::alias)

type keypaths = Step of action entry list * keypaths entry list

let print_keypaths kps =
  let rec aux prefix (Step (l, konts)) =
    String.concat "\n" (
       (List.map (fun x ->
         prefix ^ pr_keymod x.mods ^ x.keyname ^ "  " ^ x.doc ) l) @
       (List.map (fun x ->
         aux (prefix^pr_keymod x.mods^x.keyname^" ") x.contents) konts)) in
  aux "  " kps

let empty = Step([],[])

let frontier (Step(l1,l2)) =
  List.map (fun x -> pr_keymod x.mods ^ x.keyname) l1 @
  List.map (fun x -> pr_keymod x.mods ^ x.keyname) l2

let insert kps name enter_syms bindings =
  let rec aux kps enter_syms =
    match enter_syms, kps with
    | [], Step (el, konts) -> Step (List.flatten bindings @ el, konts)
    | (mods, key, keyname)::gs, Step (el, konts) ->
         if List.exists (fun { key = k; mods = m } -> key = k && mods = m) konts
         then
           let konts =
             List.map
               (fun ({ key = k; contents } as x) ->
                 if key <> k then x else { x with contents = aux contents gs })
             konts in
           Step(el,konts)
         else
           let kont =
             { mods; key; keyname; doc = name; contents = aux empty gs } in
           Step(el, kont::konts) in
  aux kps enter_syms

let run_action gui group name =
  ((actiong gui group)#get_action name)#activate ()

let run key gui action status =
  match action with
  | Callback f -> f gui; status
  | Action(group, name) -> run_action gui group name; status
  | Edit f ->
      let b = (ct gui).script#source_buffer in
      let i = b#get_iter_at_mark `INSERT in
      let status = f status b i (run_action gui) in
      if not status.sel then
        b#place_cursor ~where:(b#get_iter_at_mark `SEL_BOUND);
      status
  | Motion f ->
      let b, script = (ct gui).script#source_buffer, (ct gui).script in
      let sel_mode = status.sel || List.mem `SHIFT (GdkEvent.Key.state key) in
      let i =
        if sel_mode then b#get_iter_at_mark `SEL_BOUND
        else b#get_iter_at_mark `INSERT in
      let where, status = f status i in
      let sel_mode = status.sel || List.mem `SHIFT (GdkEvent.Key.state key) in
      if sel_mode then (b#move_mark `SEL_BOUND ~where; script#scroll_mark_onscreen `SEL_BOUND)
      else (b#place_cursor ~where; script#scroll_mark_onscreen `INSERT);
      status

let emacs = empty 

let emacs = insert emacs "Emacs" [] [
  (* motion *)
  mkE _e "e" "Move to end of line" (Motion(fun s i ->
    (if not i#ends_line then i#forward_to_line_end else i),
    { s with move = None }));
  mkE _a "a" "Move to beginning of line" (Motion(fun s i ->
    (i#set_line_offset 0), { s with move = None }));
  mkE ~mods:mM _e "e" "Move to end of sentence" (Motion(fun s i ->
    i#forward_sentence_end, { s with move = None }));
  mkE ~mods:mM _a "a" "Move to beginning of sentence" (Motion(fun s i ->
    i#backward_sentence_start, { s with move = None }));
  mkE _n "n" "Move to next line" ~alias:[[],_Down,"DOWN"] (Motion(fun s i ->
    let orig_off = Option.default i#line_offset s.move in
    let i = i#forward_line in
    let new_off = min (i#chars_in_line - 1) orig_off in
    (if new_off > 0 then i#set_line_offset new_off else i),
    { s with move = Some orig_off }));
  mkE _p "p" "Move to previous line" ~alias:[[],_Up,"UP"] (Motion(fun s i ->
    let orig_off = Option.default i#line_offset s.move in
    let i = i#backward_line in
    let new_off = min (i#chars_in_line - 1) orig_off in
    (if new_off > 0 then i#set_line_offset new_off else i),
    { s with move = Some orig_off }));
  mkE _f "f" "Forward char" ~alias:[[],_Right,"RIGHT"]
    (Motion(fun s i -> i#forward_char, { s with move = None }));
  mkE _b "b" "Backward char" ~alias:[[],_Left,"LEFT"]
    (Motion(fun s i -> i#backward_char, { s with move = None }));
  mkE ~mods:mM _f "f" "Forward word" ~alias:[mC,_Right,"RIGHT"]
    (Motion(fun s i -> i#forward_word_end, { s with move = None }));
  mkE ~mods:mM _b "b" "Backward word" ~alias:[mC,_Left,"LEFT"]
    (Motion(fun s i -> i#backward_word_start, { s with move = None }));
  mkE _space "SPC" "Set mark" ~alias:[mC,_at,"@"] (Motion(fun s i ->
    if s.sel = false then i, { s with sel = true }
    else i, { s with sel = false } ));
  (* edits *)
  mkE ~mods:mM _w "w" "Copy selected region" (Edit(fun s b i run ->
    if sel_nonempty b then
      let txt = get_sel_txt b in
      run "Edit" "Copy";
      { s with kill = Some(txt,false); sel = false }
    else s));
  mkE _w "w" "Kill selected region" (Edit(fun s b i run ->
    if sel_nonempty b then
      let txt = get_sel_txt b in
      run "Edit" "Cut";
      { s with kill = Some(txt,false); sel = false }
    else s));
  mkE _k "k" "Kill untill the end of line" (Edit(fun s b i _ ->
    let already_killed = match s.kill with Some (k,true) -> k | _ -> "" in
    let k =
      if i#ends_line then begin
        b#delete ~start:i ~stop:i#forward_char; "\n"
      end else begin 
        let k = b#get_text ~start:i ~stop:i#forward_to_line_end () in
        b#delete ~start:i ~stop:i#forward_to_line_end; k
      end in
    { s with kill = Some (already_killed ^ k,true) }));
  mkE ~mods:mM _d "d" "Kill next word" (Edit(fun s b i _ ->
    let already_killed = match s.kill with Some (k,true) -> k | _ -> "" in
    let k =
      let k = b#get_text ~start:i ~stop:i#forward_word_end () in
      b#delete ~start:i ~stop:i#forward_word_end; k in
    { s with kill = Some (already_killed ^ k,true) }));
  mkE ~mods:mM _k "k" "Kill until sentence end" (Edit(fun s b i _ ->
    let already_killed = match s.kill with Some (k,true) -> k | _ -> "" in
    let k =
      let k = b#get_text ~start:i ~stop:i#forward_sentence_end () in
      b#delete ~start:i ~stop:i#forward_sentence_end; k in
    { s with kill = Some (already_killed ^ k,true) }));
  mkE ~mods:mM _BackSpace "DELBACK" "Kill word before cursor"
    (Edit(fun s b i _ ->
    let already_killed = match s.kill with Some (k,true) -> k | _ -> "" in
    let k =
      let k = b#get_text ~start:i ~stop:i#backward_word_start () in
      b#delete ~start:i ~stop:i#backward_word_start; k in
    { s with kill = Some (already_killed ^ k,true) }));
  mkE _d "d" "Delete next character" (Edit(fun s b i _ ->
    b#delete ~start:i ~stop:i#forward_char; s));
  mkE _y "y" "Yank killed text back " (Edit(fun s b i _ ->
    let k, s = match s.kill with
    | Some (k,_) -> k, { s with kill = Some (k,false) }
    | _ -> "", s in
    b#insert ~iter:i k;
    s));
  (* misc *)
  mkE _underscore "_" "Undo" (Action("Edit", "Undo"));
  mkE _g "g" "Esc" (Callback(fun gui -> (ct gui).finder#hide ()));
  mkE _s "s" "Search" (Callback(fun gui ->
    if (ct gui).finder#coerce#misc#visible
    then run_action gui "Edit" "Find Next"
    else run_action gui "Edit" "Find"));
  mkE _s "r" "Search backward" (Callback(fun gui ->
    if (ct gui).finder#coerce#misc#visible
    then run_action gui "Edit" "Find Previous"
    else run_action gui "Edit" "Find"));
  ]

let emacs = insert emacs "Emacs" [mC,_x,"x"] [
  mkE _s "s" "Save" (Action("File", "Save"));
  mkE _c "c" "Quit" (Action("File", "Quit"));
  mkE _f "f" "Open" (Action("File", "Open"));
  mkE ~mods:[] _u "u" "Undo" (Action("Edit", "Undo"));
  ]
  
let pg = insert emacs "Proof General" [mC,_c,"c"] [
  mkE _Return "RET" "Go to" (Action("Navigation", "Go to"));
  mkE _n "n" "Advance 1 sentence" (Action("Navigation", "Forward"));
  mkE _u "u" "Retract 1 sentence" (Action("Navigation", "Backward"));
  mkE _b "b" "Advance" (Action("Navigation", "End"));
  mkE _r "r" "Restart" (Action("Navigation", "Start"));
  mkE _c "c" "Stop"    (Action("Navigation", "Interrupt"));
  ]

let command gui c =
  let command = (ct gui).command in
  let script = (ct gui).script in
  let term =
    let i, j = script#source_buffer#selection_bounds in
    if i#equal j then None
    else Some (script#buffer#get_text ~start:i ~stop:j ()) in
  command#show;
  command#new_query ~command:c ?term ()

let pg = insert pg "Proof General" [mC,_c,"c"; mC,_a,"a"] [
  mkE _p "p" "Print" (Callback (fun gui -> command gui "Print"));
  mkE _c "c" "Check" (Callback (fun gui -> command gui "Check"));
  mkE _b "b" "About" (Callback (fun gui -> command gui "About"));
  mkE _a "a" "Search About" (Callback (fun gui -> command gui "SearchAbout"));
  mkE _o "o" "Search Pattern" (Callback (fun gui->command gui "SearchPattern"));
  mkE _l "l" "Locate" (Callback (fun gui -> command gui "Locate"));
  mkE _Return "RET" "match template" (Action("Templates","match"));
  ]

let empty = { sel = false; kill = None; move = None }

let find gui (Step(here,konts)) t =
  (* hack: ^c does copy in clipboard *)
  let sel_nonempty () = sel_nonempty (ct gui).script#source_buffer in
  let k = GdkEvent.Key.keyval t in
  if k = _x && mod_of t mC && sel_nonempty () then
    ignore(run t gui (Action("Edit","Cut")) empty)
  else
    if k = _c && mod_of t mC && sel_nonempty () then
      ignore(run t gui (Action("Edit","Copy")) empty);
    let cmp { key; mods } = key = k && mod_of t mods in
    try `Do (List.find cmp here) with Not_found ->
    try `Cont (List.find cmp konts).contents with Not_found -> `NotFound

let init w nb ags =
  let gui = { notebook = nb; action_groups = ags } in
  let cur = ref pg in
  let status = ref empty in
  let reset () = eprintf "reset\n%!"; cur := pg in
  ignore(w#event#connect#key_press ~callback:(fun t ->
    let on_current_term f =
      let term = try Some nb#current_term with Invalid_argument _ -> None in
      match term with None -> false | Some t -> f t
    in
    on_current_term (fun x ->
    if x.script#misc#get_property "has-focus" <> `BOOL true
    then false
    else begin
    eprintf "got key %s\n%!" (pr_key t);
    if current.nanoPG then begin
      match find gui !cur t with
      | `Do e ->
           eprintf "run (%s) %s on %s\n%!" e.keyname e.doc (pr_status !status);
           status := run t gui e.contents !status; reset (); true
      | `Cont c ->
           flash_info ("Waiting one of " ^ String.concat " " (frontier c));
           cur := c; true
      | `NotFound -> reset (); false
    end else false
  end)));
  ignore(w#event#connect#button_press ~callback:(fun t -> reset (); false))



let get_documentation () = print_keypaths pg