[Dive] Add a show/hide feature
Showing
- src/plugins/dive/build.ml 81 additions, 88 deletionssrc/plugins/dive/build.ml
- src/plugins/dive/build.mli 4 additions, 0 deletionssrc/plugins/dive/build.mli
- src/plugins/dive/graph_types.mli 2 additions, 1 deletionsrc/plugins/dive/graph_types.mli
- src/plugins/dive/imprecision_graph.ml 51 additions, 0 deletionssrc/plugins/dive/imprecision_graph.ml
- src/plugins/dive/imprecision_graph.mli 4 additions, 0 deletionssrc/plugins/dive/imprecision_graph.mli
- src/plugins/dive/node_kind.ml 68 additions, 2 deletionssrc/plugins/dive/node_kind.ml
- src/plugins/dive/node_kind.mli 29 additions, 0 deletionssrc/plugins/dive/node_kind.mli
- src/plugins/dive/server_interface.ml 21 additions, 0 deletionssrc/plugins/dive/server_interface.ml
- src/plugins/dive/simple_deps.ml 65 additions, 0 deletionssrc/plugins/dive/simple_deps.ml
Loading
Please register or sign in to comment