From 8f0260c89e45f9a5b36fedb9488ef56095c4f6fe Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Wed, 22 Jul 2020 14:19:19 +0200
Subject: [PATCH] [Extlib] add function format_string_of_stag
---
src/libraries/stdlib/extlib.ml | 4 ++++
src/libraries/stdlib/extlib.mli | 7 +++++++
src/plugins/gui/pretty_source.ml | 10 ++--------
src/plugins/gui/wtext.ml | 5 +----
src/plugins/metrics/metrics_base.ml | 10 ++--------
src/plugins/server/jbuffer.ml | 5 +----
6 files changed, 17 insertions(+), 24 deletions(-)
diff --git a/src/libraries/stdlib/extlib.ml b/src/libraries/stdlib/extlib.ml
index 0714b72b4c9..04d1facd71e 100644
--- a/src/libraries/stdlib/extlib.ml
+++ b/src/libraries/stdlib/extlib.ml
@@ -512,6 +512,10 @@ let html_escape s =
) s ;
Buffer.contents buf
+let format_string_of_stag = function
+ | Format.String_tag tag -> tag
+ | _ -> raise (Invalid_argument "unsupported tag extension")
+
(* ************************************************************************* *)
(** Comparison functions *)
(* ************************************************************************* *)
diff --git a/src/libraries/stdlib/extlib.mli b/src/libraries/stdlib/extlib.mli
index a4ddfca43aa..7a1204e843c 100644
--- a/src/libraries/stdlib/extlib.mli
+++ b/src/libraries/stdlib/extlib.mli
@@ -320,6 +320,13 @@ val strip_underscore: string -> string
val html_escape: string -> string
+(** [format_string_of_stag stag] returns the string corresponding to [stag],
+ or raises an exception if the tag extension is unsupported.
+
+ @since Frama-C+dev
+ *)
+val format_string_of_stag: Format.stag -> string
+
(* ************************************************************************* *)
(** {2 Performance} *)
(* ************************************************************************* *)
diff --git a/src/plugins/gui/pretty_source.ml b/src/plugins/gui/pretty_source.ml
index d86d8befd03..fae7a1f6c75 100644
--- a/src/plugins/gui/pretty_source.ml
+++ b/src/plugins/gui/pretty_source.ml
@@ -275,20 +275,14 @@ let localizable_from_locs state ~file ~line =
let buffer_formatter state source =
let starts = Stack.create () in
let emit_open_tag s =
- let s = match s with
- | Format.String_tag tag -> tag
- | _ -> raise (Invalid_argument "unsupported tag extension")
- in
+ let s = Extlib.format_string_of_stag s in
(* Ignore tags that are not ours *)
if Extlib.string_prefix "guitag:" s then
Stack.push (source#end_iter#offset, Tag.get s) starts ;
""
in
let emit_close_tag s =
- let s = match s with
- | Format.String_tag tag -> tag
- | _ -> raise (Invalid_argument "unsupported tag extension")
- in
+ let s = Extlib.format_string_of_stag s in
(try
if Extlib.string_prefix "guitag:" s then
let (p,sid) = Stack.pop starts in
diff --git a/src/plugins/gui/wtext.ml b/src/plugins/gui/wtext.ml
index f8252175c62..7bfe557c975 100644
--- a/src/plugins/gui/wtext.ml
+++ b/src/plugins/gui/wtext.ml
@@ -244,10 +244,7 @@ class text ?(autoscroll=false) ?(width=80) ?(indent=60) () =
end
method private open_tag name =
- let name = match name with
- | Format.String_tag str -> str
- | _ -> raise (Invalid_argument "unsupported tag extension")
- in
+ let name = Extlib.format_string_of_stag name in
self#flush () ; style <- self#tag name :: style ; ""
method private close_tag _name =
diff --git a/src/plugins/metrics/metrics_base.ml b/src/plugins/metrics/metrics_base.ml
index b847b1b185d..c4c0934db60 100644
--- a/src/plugins/metrics/metrics_base.ml
+++ b/src/plugins/metrics/metrics_base.ml
@@ -26,16 +26,10 @@ open Cil_types (* vname, vaddrof *)
(* Formatting html with Format.formatters *)
let html_stag_functions =
let mark_open_stag t =
- let t = match t with
- | Format.String_tag tag -> tag
- | _ -> raise (Invalid_argument "unsupported tag extension")
- in
+ let t = Extlib.format_string_of_stag t in
Format.sprintf "<%s>" t
and mark_close_stag t =
- let t = match t with
- | Format.String_tag tag -> tag
- | _ -> raise (Invalid_argument "unsupported tag extension")
- in
+ let t = Extlib.format_string_of_stag t in
try
let index = String.index t ' ' in
Format.sprintf "</%s>" (String.sub t 0 index)
diff --git a/src/plugins/server/jbuffer.ml b/src/plugins/server/jbuffer.ml
index ced67a4aa78..f7ca9ebbfe0 100644
--- a/src/plugins/server/jbuffer.ml
+++ b/src/plugins/server/jbuffer.ml
@@ -41,10 +41,7 @@ let flush buffer () =
Buffer.clear t
let push_tag buffer stag =
- let tag = match stag with
- | Format.String_tag tag -> tag
- | _ -> raise (Invalid_argument "unsupported tag extension")
- in
+ let tag = Extlib.format_string_of_stag stag in
flush buffer () ;
buffer.stack <- ( tag , buffer.rjson ) :: buffer.stack ;
buffer.rjson <- []
--
GitLab