diff --git a/src/libraries/stdlib/extlib.ml b/src/libraries/stdlib/extlib.ml index 0714b72b4c9816a4c8a2f4453104fb99bc2fbdab..04d1facd71e8c7df8b9a21aef7b9b054ff26f70b 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 a4ddfca43aa2076d688261de6b388cdb12060f7a..7a1204e843cf57bea0b27b12844c5a73774360b1 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 d86d8befd03d65240c91b4b29ab84517e79a44c2..fae7a1f6c75b9dad6da3f7d676e01af913aca608 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 f8252175c62ce1f3cc206dfb944786818e114941..7bfe557c97514b4af670d6cb0b61f7de097c69dc 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 b847b1b185d85b1e926a23006df37b2a01ea46e2..c4c0934db605687aeb685d16abaebc37a0b4e5d6 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 ced67a4aa781bdc4628ab030e68646b52da9d46b..f7ca9ebbfe05418e06440810bca2103881afd3b3 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 <- []