package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file wtext.ml

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
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
(**************************************************************************)
(*                                                                        *)
(*  This file is part of Frama-C.                                         *)
(*                                                                        *)
(*  Copyright (C) 2007-2024                                               *)
(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
(*         alternatives)                                                  *)
(*                                                                        *)
(*  you can redistribute it and/or modify it under the terms of the GNU   *)
(*  Lesser General Public License as published by the Free Software       *)
(*  Foundation, version 2.1.                                              *)
(*                                                                        *)
(*  It is distributed in the hope that it will be useful,                 *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
(*  GNU Lesser General Public License for more details.                   *)
(*                                                                        *)
(*  See the GNU Lesser General Public License version 2.1                 *)
(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
(*                                                                        *)
(**************************************************************************)

module Rangemap = Rgmap

(* -------------------------------------------------------------------------- *)
(* --- Text with Tagging Formatter                                        --- *)
(* -------------------------------------------------------------------------- *)

type tag =
  | TAG of GText.tag
  | MARK of int * string
  | LINK of int * string
  | PLAIN

let rec filter_tags tgs = function
  | [] -> tgs
  | TAG t :: style -> filter_tags (t::tgs) style
  | (MARK _ | LINK _ | PLAIN) :: style -> filter_tags tgs style

let split_tag tag =
  let rec lookup tag k n =
    if k < n then
      if tag.[k] = ':'
      then String.sub tag 0 k , String.sub tag (k+1) (n-k-1)
      else lookup tag (succ k) n
    else tag,""
  in lookup tag 0 (String.length tag)

let css_sheet = [
  "ul" , [ `UNDERLINE `SINGLE ];
  "st" , [ `STRIKETHROUGH true ];
  "bf" , [ `WEIGHT `BOLD ];
  "it" , [ `STYLE `ITALIC ];
  "red" , [ `FOREGROUND "red" ];
  "blue" , [ `FOREGROUND "blue" ];
  "green" , [ `FOREGROUND "darkgreen" ];
  "orange" , [ `FOREGROUND "orange" ];
  "hover" , [ `BACKGROUND "lightblue" ];
  "link" , [ `FOREGROUND "blue" ];
]

type 'a entry = int * int * 'a

let rec fire e = function [] -> () | f::fs -> f e ; fire e fs

class type ['a] marker =
  object
    method set_style : GText.tag_property list -> unit
    method set_hover : GText.tag_property list -> unit
    method connect : (GdkEvent.Button.t -> 'a entry -> unit) -> unit
    method on_click : ('a entry -> unit) -> unit
    method on_double_click : ('a entry -> unit) -> unit
    method on_right_click : ('a entry -> unit) -> unit
    method on_shift_click : ('a entry -> unit) -> unit
    method on_add : ('a entry -> unit) -> unit
    method wrap : (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a -> unit
    method mark : 'b. 'a -> (Format.formatter -> 'b -> unit) -> Format.formatter -> 'b -> unit
    method add : 'a entry -> unit
  end

type style = NoStyle | StyleSet | Style of GText.tag_property list

let configure tag = function
  | NoStyle -> NoStyle
  | StyleSet -> StyleSet
  | Style [] -> NoStyle
  | Style sty -> tag#set_properties sty ; StyleSet

(* -------------------------------------------------------------------------- *)
(* --- Monomorphic Marker                                                 --- *)
(* -------------------------------------------------------------------------- *)

type blind = {
  hover : GText.tag ;
  click : (bool -> GdkEvent.Button.t -> unit) ;
}

type registry = blind entry -> unit
type wrapper =
  (int -> int -> unit) ->
  (Format.formatter -> unit) -> Format.formatter -> unit

class ['a] poly_marker
    (buffer : GText.buffer)
    (registry : registry)
    (wrapper : wrapper)
  =
  let style = buffer#create_tag [] in
  let hover = buffer#create_tag [] in
  object(self)

    (*--- Style Configuration ---*)

    val mutable style_props = NoStyle
    val mutable hover_props = Style (List.assoc "hover" css_sheet)
    val mutable to_configure = true

    method set_style sty = assert to_configure ; style_props <- Style sty
    method set_hover sty = assert to_configure ; hover_props <- Style sty

    method private configure =
      if to_configure then
        begin
          style_props <- configure style style_props ;
          hover_props <- configure hover hover_props ;
          to_configure <- false ;
        end

    val mutable demon : (GdkEvent.Button.t -> 'a entry -> unit) list = []
    val mutable demon_click  : ('a entry -> unit) list = []
    val mutable demon_double : ('a entry -> unit) list = []
    val mutable demon_right  : ('a entry -> unit) list = []
    val mutable demon_shift  : ('a entry -> unit) list = []
    val mutable demon_added  : ('a entry -> unit) list = []

    (*--- Signal Connection ---*)

    method connect f = demon <- demon @ [f]
    method on_click d = demon_click <- demon_click @ [d]
    method on_double_click d = demon_double <- demon_double @ [d]
    method on_right_click d = demon_right <- demon_right @ [d]
    method on_shift_click d = demon_shift <- demon_shift @ [d]
    method on_add d = demon_added <- demon_added @ [d]

    (*--- Adding ---*)

    method add (e : 'a entry) =
      begin
        self#configure ;
        let (p,q,_) = e in
        if style_props = StyleSet then
          begin
            let start = buffer#get_iter (`OFFSET p) in
            let stop = buffer#get_iter (`OFFSET q) in
            buffer#apply_tag style ~start ~stop
          end ;
        let click double evt =
          List.iter (fun f -> f evt e) demon ;
          if double then fire e demon_double else
            let state = GdkEvent.Button.state evt in
            if Gdk.Convert.test_modifier `BUTTON3 state
            then fire e demon_right else
            if Gdk.Convert.test_modifier `BUTTON1 state
            then if Gdk.Convert.test_modifier `SHIFT state
              then fire e demon_shift
              else fire e demon_click
        in
        registry (p,q,{ hover ; click }) ;
        ignore (fire e demon_added) ;
      end

    method wrap pp (fmt:Format.formatter) (w:'a) : unit =
      self#mark w pp fmt w

    method mark :
      'b. 'a ->
      (Format.formatter -> 'b -> unit) -> Format.formatter -> 'b -> unit =
      fun e pp fmt w ->
      wrapper (fun p q -> self#add (p,q,e)) (fun fmt -> pp fmt w) fmt

  end

(* -------------------------------------------------------------------------- *)
(* --- Text Widget                                                        --- *)
(* -------------------------------------------------------------------------- *)

class text ?(autoscroll=false) ?(width=80) ?(indent=60) () =
  let buffer = GText.buffer () in
  let react = buffer#create_tag [] in
  let view = GText.view ~buffer
      ~editable:false ~cursor_visible:false
      ~justification:`LEFT
      ~wrap_mode:`NONE
      ~accepts_tab:false
      ~show:true () in
  let scroll = GBin.scrolled_window () in
  object(self)

    val text = Buffer.create 80
    val css = Hashtbl.create 32
    val marks : (string,int -> int -> unit) Hashtbl.t = Hashtbl.create 32
    val mutable links : string marker option = None
    val mutable width = width
    val mutable hrule = ""
    val mutable ruled = false
    val mutable indent = indent
    val mutable hid = 0
    val mutable autoscroll = autoscroll
    val mutable style = []
    val mutable fmtref = None
    val mutable reactive = false
    val mutable index : blind Rangemap.t = Rangemap.empty
    val mutable hovered = None
    val mutable double = false

    (* -------------------------------------------------------------------------- *)
    (* --- Text Initializer                                                   --- *)
    (* -------------------------------------------------------------------------- *)

    initializer
      begin
        (* Ignore default pango contextual menu (copy/cut/paste etc...), as this
           widget is read-only *)
        ignore (view#event#connect#button_press
                  ~callback:(fun ev -> GdkEvent.Button.button ev = 3));
        scroll#add view#coerce
      end

    (* -------------------------------------------------------------------------- *)
    (* --- Text Formatter                                                     --- *)
    (* -------------------------------------------------------------------------- *)

    method private flush () =
      if Buffer.length text > 0 then
        begin
          let s = Wutil.to_utf8 (Buffer.contents text) in
          Buffer.clear text ;
          let tags = filter_tags [] style in
          let iter = buffer#end_iter in
          buffer#insert ~tags ~iter s ;
          if reactive then
            let start,stop = buffer#bounds in
            buffer#apply_tag react ~start ~stop ;
        end

    method private open_tag name =
      let name = Extlib.format_string_of_stag name in
      self#flush () ; style <- self#tag name :: style ; ""

    method private close_tag _name =
      self#flush () ; match style with
      | [] -> ""
      | MARK(p,mrk) :: sty -> style <- sty ; self#mark p mrk ; ""
      | LINK(p,lnk) :: sty -> style <- sty ; self#link p lnk ; ""
      | (TAG _ | PLAIN) :: sty -> style <- sty ; ""

    method fmt = match fmtref with Some fmt -> fmt | None ->
      let open Format in
      let output_string s a b = if b > 0 then Buffer.add_substring text s a b in
      let fmt = Format.make_formatter output_string self#flush in
      let tagger = pp_get_formatter_stag_functions fmt () in
      pp_set_formatter_stag_functions fmt
        { tagger with
          mark_open_stag = self#open_tag;
          mark_close_stag = self#close_tag ;
        } ;
      Format.pp_set_print_tags fmt false ;
      Format.pp_set_mark_tags fmt true ;
      Format.pp_set_margin fmt width ;
      Format.pp_set_max_indent fmt indent ;
      fmtref <- Some fmt ; fmt

    method offset = self#flush () ; buffer#end_iter#offset

    method set_width w =
      width <- w ; hrule <- "" ;
      match fmtref with None -> () | Some fmt ->
        Format.pp_set_margin fmt w

    method set_indent p =
      indent <- p ; match fmtref with None -> () | Some fmt ->
        Format.pp_set_max_indent fmt p

    (* -------------------------------------------------------------------------- *)
    (* --- Link & Marking                                                     --- *)
    (* -------------------------------------------------------------------------- *)

    method links =
      match links with
      | Some marker -> marker
      | None ->
        let marker = self#marker in
        marker#set_style (List.assoc "link" css_sheet) ;
        marker#set_hover (List.assoc "hover" css_sheet) ;
        links <- Some marker ; marker

    method private link p name =
      let q = buffer#end_iter#offset in
      self#links#add (p,q,name)

    method private mark p name =
      let q = buffer#end_iter#offset in
      List.iter (fun f -> f p q) (Hashtbl.find_all marks name)

    method on_link f = self#links#on_click (fun (_,_,lnk) -> f lnk)

    method wrap f pp fmt =
      begin
        let sid = hid <- succ hid ; Printf.sprintf ">%X" hid in
        Hashtbl.add marks sid (fun p q -> Hashtbl.remove marks sid ; f p q) ;
        Format.pp_open_stag fmt (Format.String_tag sid) ;
        let () = pp fmt in
        Format.pp_close_stag fmt () ;
      end

    (* -------------------------------------------------------------------------- *)
    (* --- Tag Marking                                                        --- *)
    (* -------------------------------------------------------------------------- *)

    method private css_style name props =
      let sty = TAG(buffer#create_tag ~name props) in
      Hashtbl.replace css name sty ; sty

    method private tag name =
      if Hashtbl.mem marks name then MARK(buffer#end_iter#offset,name)
      else
        try Hashtbl.find css name
        with Not_found ->
        try self#css_style name (List.assoc name css_sheet)
        with Not_found ->
          begin
            match split_tag name with
            | "fg",color -> self#css_style name [ `FOREGROUND color ]
            | "bg",color -> self#css_style name [ `BACKGROUND color ]
            | "link",name -> LINK(buffer#end_iter#offset,name)
            | _ -> PLAIN
          end

    method set_css sheet =
      List.iter (fun (name,tags) -> ignore (self#css_style name tags)) sheet

    method set_style name p q =
      match self#tag name with
      | PLAIN | LINK _ | MARK _ -> ()
      | TAG tag ->
        let start = buffer#get_iter (`OFFSET p) in
        let stop = buffer#get_iter (`OFFSET q) in
        buffer#apply_tag tag ~start ~stop

    method remove_style name p q =
      match Hashtbl.find css name with
      | PLAIN | LINK _ | MARK _ -> ()
      | TAG tag ->
        let start = buffer#get_iter (`OFFSET p) in
        let stop = buffer#get_iter (`OFFSET q) in
        buffer#remove_tag tag ~start ~stop

    method remove_all names =
      let start,stop = buffer#bounds in
      List.iter
        (fun name ->
           match Hashtbl.find css name with
           | TAG tag -> buffer#remove_tag tag ~start ~stop
           | PLAIN | LINK _ | MARK _ -> ())
        names

    (* -------------------------------------------------------------------------- *)
    (* --- Hover & Mark Dispatcher                                            --- *)
    (* -------------------------------------------------------------------------- *)

    method private set_reactive =
      if not reactive then
        let callback ~origin:_ evt iter =
          (* return false to propagate events *)
          match GdkEvent.get_type evt with
          | `BUTTON_PRESS -> double <- false ; false
          | `TWO_BUTTON_PRESS -> double <- true ; false
          | `BUTTON_RELEASE ->
            begin
              match hovered with
              | None -> ()
              | Some (_,_,blind) ->
                blind.click double (GdkEvent.Button.cast evt)
            end ; false
          | `MOTION_NOTIFY ->
            let offset = GtkText.Iter.get_offset iter in
            let entry =
              try Some(Rangemap.find offset offset index)
              with Not_found -> None
            in self#hover entry ; false
          | _ -> false
        in ( ignore (react#connect#event ~callback) ; reactive <- true )

    method private hover h =
      match hovered , h with
      | Some e0 , Some e when e == e0 -> ()
      | None , None -> ()
      | _ ->
        begin
          (match hovered with None -> () | Some (_,_,{hover}) ->
              let start,stop = buffer#bounds in
              buffer#remove_tag hover ~start ~stop) ;
          (match h with None -> () | Some (a,b,{hover}) ->
              let start = buffer#get_iter (`OFFSET a) in
              let stop = buffer#get_iter (`OFFSET b) in
              self#hover None ;
              buffer#apply_tag hover ~start ~stop) ;
          hovered <- h
        end

    method private register e =
      index <- Rangemap.add e index

    (* -------------------------------------------------------------------------- *)
    (* --- User API                                                           --- *)
    (* -------------------------------------------------------------------------- *)

    method set_autoscroll s = autoscroll <- s

    method printf : 'a. ?scroll:bool ->
      ('a,Format.formatter,unit) format -> 'a =
      fun ?(scroll=autoscroll) text ->
      (* Save current number of lines in the buffer *)
      let line = view#buffer#line_count in
      let finally fmt =
        Format.pp_print_flush fmt () ;
        Hashtbl.clear marks ;
        hid <- 0 ;
        ruled <- false ;
        if scroll then
          (* scrolling must be performed asynchronously using Gtk_helper.later,
             otherwise it will not take into account the newly added text. *)
          Wutil.later (self#scroll ~line)
      in
      Format.kfprintf finally self#fmt text

    method hrule =
      if not ruled then
        begin
          if String.length hrule = 0 then
            hrule <- String.make width '-' ;
          Format.pp_print_string self#fmt hrule ;
          Format.pp_print_newline self#fmt () ;
          ruled <- true ;
        end

    method lines = view#buffer#line_count

    method scroll ?line () =
      let buf = view#buffer in
      let line = match line with Some l -> l | None -> buf#line_count in
      let iter = buf#get_iter_at_char ~line 0 in
      ignore (view#scroll_to_iter ~use_align:true ~yalign:0.0 iter)

    method select ?(scroll=false) (p:int) (q:int) =
      let buffer = view#buffer in
      let start = buffer#get_iter (`OFFSET p) in
      let stop = buffer#get_iter (`OFFSET q) in
      buffer#select_range start stop ;
      ignore (view#scroll_to_iter ~use_align:scroll ~yalign:0.3 start)

    method clear =
      begin
        Format.pp_print_flush self#fmt () ;
        Hashtbl.clear marks ; hid <- 0 ;
        buffer#delete ~start:buffer#start_iter ~stop:buffer#end_iter ;
        index <- Rangemap.empty ;
        self#hover None ;
      end

    method coerce = scroll#coerce
    method widget = (self :> Widget.t)
    method set_enabled = Wutil.set_enabled scroll
    method set_visible = Wutil.set_visible scroll

    method set_font = Wutil.set_font view
    method set_monospace = Wutil.set_monospace view

    method marker : 'a. 'a marker =
      let h = new poly_marker buffer self#register self#wrap in
      self#set_reactive ;
      (h :> _ marker)

    method get_view = view

  end
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct