diff --git a/src/plugins/gui/filetree.ml b/src/plugins/gui/filetree.ml index 7dbc3973b988555cdc734144379c11067bd03304..4f7eaadff93fcb86334575d288d1f757d3d4efe1 100644 --- a/src/plugins/gui/filetree.ml +++ b/src/plugins/gui/filetree.ml @@ -104,7 +104,7 @@ struct type custom_tree = {finfo: TREE.t; mutable sons: custom_tree array; - mutable parent: custom_tree option; + parent: custom_tree option; fidx: int (* invariant: parent.(fidx)==myself *) } let inbound i a = i>=0 && i<Array.length a @@ -236,7 +236,7 @@ end module MYTREE = struct type storage = { mutable name : string; - mutable globals: global array; + globals: global array; mutable strikethrough: bool} diff --git a/src/plugins/gui/source_manager.ml b/src/plugins/gui/source_manager.ml index 7ceadddf52977b182dcf49b30d74b615c52c7058..d3d250910729b73520a966bd85f8ccd21d627605 100644 --- a/src/plugins/gui/source_manager.ml +++ b/src/plugins/gui/source_manager.ml @@ -21,7 +21,6 @@ (**************************************************************************) type tab = { - tab_name : string ; tab_file : Datatype.Filepath.t ; tab_page : int ; tab_select : line:int -> unit ; @@ -184,7 +183,6 @@ let load_file w ?title ~(filename : Datatype.Filepath.t) ?(line=(-1)) ~click_cb )); let tab = { tab_file = filename ; - tab_name = name ; tab_select = select_line ; tab_page = page_num ; tab_source_view = original_source_view; diff --git a/src/plugins/gui/warning_manager.ml b/src/plugins/gui/warning_manager.ml index f9f95f0b838214af73334c3a4450c47c52fcde67..4077c05da035a4eede4aa8f4f73f365e9e84b2c0 100644 --- a/src/plugins/gui/warning_manager.ml +++ b/src/plugins/gui/warning_manager.ml @@ -27,8 +27,7 @@ let scope = function type row = Log.event type t = - { widget: (int*row) Wtable.columns; - append : row -> unit; + { append : row -> unit; clear : unit -> unit;} module Data = Indexer.Make( @@ -78,7 +77,7 @@ let make ~packing ~callback = (fun (_,{evt_message=m}) -> [`TEXT m]) in w#on_click (fun (_,w) c -> callback w c); - {widget=w;append=append;clear=clear} + {append=append;clear=clear} let append t message = t.append message