diff --git a/src/kernel_services/ast_printing/printer_tag.ml b/src/kernel_services/ast_printing/printer_tag.ml
index 6684aa01fc592cf9b165b1fe258fcd8c704e7dbc..e73b16d8b087d9c9b6901a7e548579606ab489a9 100644
--- a/src/kernel_services/ast_printing/printer_tag.ml
+++ b/src/kernel_services/ast_printing/printer_tag.ml
@@ -584,7 +584,7 @@ struct
 
     method! pp_while ~stmt ~cond fmt =
       Format.fprintf fmt "@{<%s>%t@}"
-        (Tag.create (PStmt(Option.get self#current_kf,stmt)))
+        (Tag.create (PStmtStart(Option.get self#current_kf,stmt)))
         (super#pp_while ~stmt ~cond)
 
     method! next_stmt next fmt current =
diff --git a/src/kernel_services/ast_printing/printer_tag.mli b/src/kernel_services/ast_printing/printer_tag.mli
index 57de33aaba62d745b1886efcaf7f2a12568ea862..d30adb07b6171ad90b0a4d7155e356217ae82ba7 100644
--- a/src/kernel_services/ast_printing/printer_tag.mli
+++ b/src/kernel_services/ast_printing/printer_tag.mli
@@ -27,18 +27,23 @@ open Cil_types
 (** The kind of object that can be selected in the source viewer. *)
 type localizable =
   | PStmt of (kernel_function * stmt)
+  (** Full statement (with attributes, annotations, etc.) *)
   | PStmtStart of (kernel_function * stmt)
+  (** Naked statement (only skind, without attributes, annotations, etc.) *)
   | PLval of (kernel_function option * kinstr * lval)
+  (** L-Values *)
   | PExp of (kernel_function option * kinstr * exp)
+  (** Non l-value expressions *)
   | PTermLval of (kernel_function option * kinstr * Property.t * term_lval)
+  (** Term l-values inside properties *)
   | PVDecl of (kernel_function option * kinstr * varinfo)
   (** Declaration and definition of variables and function. Check the type
       of the varinfo to distinguish between the various possibilities.
       If the varinfo is a global or a local, the kernel_function is the
       one in which the variable is declared. The [kinstr] argument is given
       for local variables with an explicit initializer. *)
-  | PGlobal of global (** all globals but variable declarations and function
-                          definitions. *)
+  | PGlobal of global
+  (** Global definitions except global variables and functions. *)
   | PIP of Property.t
   | PType of typ