From 0bb75da65f6410cd95e11670df676d531cd5277a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Thu, 19 Mar 2020 11:35:11 +0100
Subject: [PATCH] [server] localizable with collections
---
.../ast_printing/printer_tag.ml | 2 +-
.../ast_printing/printer_tag.mli | 2 +-
src/plugins/server/kernel_ast.ml | 21 ++++++++++++-------
3 files changed, 15 insertions(+), 10 deletions(-)
diff --git a/src/kernel_services/ast_printing/printer_tag.ml b/src/kernel_services/ast_printing/printer_tag.ml
index 9009c9ac711..898e8129f48 100644
--- a/src/kernel_services/ast_printing/printer_tag.ml
+++ b/src/kernel_services/ast_printing/printer_tag.ml
@@ -38,7 +38,7 @@ type localizable =
| PIP of Property.t
module Localizable =
- Datatype.Make
+ Datatype.Make_with_collections
(struct
include Datatype.Undefined
type t = localizable
diff --git a/src/kernel_services/ast_printing/printer_tag.mli b/src/kernel_services/ast_printing/printer_tag.mli
index befac9be01d..074ec5c58ef 100644
--- a/src/kernel_services/ast_printing/printer_tag.mli
+++ b/src/kernel_services/ast_printing/printer_tag.mli
@@ -41,7 +41,7 @@ type localizable =
definitions. *)
| PIP of Property.t
-module Localizable: Datatype.S with type t = localizable
+module Localizable: Datatype.S_with_collections with type t = localizable
val kf_of_localizable : localizable -> kernel_function option
val ki_of_localizable : localizable -> kinstr
diff --git a/src/plugins/server/kernel_ast.ml b/src/plugins/server/kernel_ast.ml
index acd12071821..21870f3dfc5 100644
--- a/src/plugins/server/kernel_ast.ml
+++ b/src/plugins/server/kernel_ast.ml
@@ -45,13 +45,18 @@ module Marker =
struct
open Printer_tag
- module Hmap = Hashtbl.Make(Localizable)
- type index = string Hmap.t * (string,localizable) Hashtbl.t
+ type index = {
+ tags : string Localizable.Hashtbl.t ;
+ locs : (string,localizable) Hashtbl.t ;
+ }
let kid = ref 0
- let index () = Hmap.create 0, Hashtbl.create 0
+ let index () = {
+ tags = Localizable.Hashtbl.create 0 ;
+ locs = Hashtbl.create 0 ;
+ }
module TYPE : Datatype.S with type t = index =
Datatype.Make
@@ -81,15 +86,15 @@ struct
| PIP _ -> Printf.sprintf "#p%d" (incr kid ; !kid)
let create loc =
- let (tags,index) = STATE.get () in
- try Hmap.find tags loc
+ let { tags ; locs } = STATE.get () in
+ try Localizable.Hashtbl.find tags loc
with Not_found ->
let tag = create_tag loc in
- Hmap.add tags loc tag ;
- Hashtbl.add index tag loc ;
+ Localizable.Hashtbl.add tags loc tag ;
+ Hashtbl.add locs tag loc ;
tag
- let lookup = Hashtbl.find (STATE.get() |> snd)
+ let lookup = Hashtbl.find (STATE.get()).locs
type t = localizable
let syntax = Sy.publish ~page:Data.page ~name:"marker"
--
GitLab