update descriptions

+ rename metas:
    "realized" => "realized_theory"
    "remove_type_symbol" => "remove_type"

Makefile.in

@@ -875,19 +875,19 @@ COQVD = $(addsuffix .vd, $(COQLIBS_FILES))
 drivers/coq-realizations.aux: Makefile
 	$(if $(QUIET),@echo 'Generate $@' &&) \
 	(echo "(* generated automatically at compilation time *)"; \
-	echo 'theory BuiltIn meta "realized" "BuiltIn", "" end'; \
+	echo 'theory BuiltIn meta "realized_theory" "BuiltIn", "" end'; \
 	for f in $(COQLIBS_INT_FILES); do \
-	echo 'theory int.'"$$f"' meta "realized" "int.'"$$f"'", "" end'; done; \
+	echo 'theory int.'"$$f"' meta "realized_theory" "int.'"$$f"'", "" end'; done; \
 	for f in $(COQLIBS_REAL_FILES); do \
-	echo 'theory real.'"$$f"' meta "realized" "real.'"$$f"'", "" end'; done; \
+	echo 'theory real.'"$$f"' meta "realized_theory" "real.'"$$f"'", "" end'; done; \
 	for f in $(COQLIBS_NUMBER_FILES); do \
-	echo 'theory number.'"$$f"' meta "realized" "number.'"$$f"'", "" end'; done; \
+	echo 'theory number.'"$$f"' meta "realized_theory" "number.'"$$f"'", "" end'; done; \
 	for f in $(COQLIBS_SET_FILES); do \
-	echo 'theory set.'"$$f"' meta "realized" "set.'"$$f"'", "" end'; done; \
+	echo 'theory set.'"$$f"' meta "realized_theory" "set.'"$$f"'", "" end'; done; \
 	for f in $(COQLIBS_SETTHEORY_FILES); do \
-	echo 'theory settheory.'"$$f"' meta "realized" "settheory.'"$$f"'", "" end'; done; \
+	echo 'theory settheory.'"$$f"' meta "realized_theory" "settheory.'"$$f"'", "" end'; done; \
 	for f in $(COQLIBS_FP_FILES); do \
-	echo 'theory floating_point.'"$$f"' meta "realized" "floating_point.'"$$f"'", "" end'; done; \
+	echo 'theory floating_point.'"$$f"' meta "realized_theory" "floating_point.'"$$f"'", "" end'; done; \
 	) > $@
 
 opt byte: $(COQVO)
@@ -990,15 +990,15 @@ drivers/pvs-realizations.aux: Makefile
 	$(if $(QUIET),@echo 'Generate $@' &&) \
 	(echo "(* generated automatically at compilation time *)"; \
 	for f in $(PVSLIBS_INT_FILES); do \
-	echo 'theory int.'"$$f"' meta "realized" "int.'"$$f"'", "" end'; done; \
+	echo 'theory int.'"$$f"' meta "realized_theory" "int.'"$$f"'", "" end'; done; \
 	for f in $(PVSLIBS_REAL_FILES); do \
-	echo 'theory real.'"$$f"' meta "realized" "real.'"$$f"'", "" end'; done; \
+	echo 'theory real.'"$$f"' meta "realized_theory" "real.'"$$f"'", "" end'; done; \
 	for f in $(PVSLIBS_LIST_FILES); do \
-	echo 'theory list.'"$$f"' meta "realized" "list.'"$$f"'", "" end'; done; \
+	echo 'theory list.'"$$f"' meta "realized_theory" "list.'"$$f"'", "" end'; done; \
 	for f in $(PVSLIBS_NUMBER_FILES); do \
-	echo 'theory number.'"$$f"' meta "realized" "number.'"$$f"'", "" end'; done; \
+	echo 'theory number.'"$$f"' meta "realized_theory" "number.'"$$f"'", "" end'; done; \
 	for f in $(PVSLIBS_FP_FILES); do \
-	echo 'theory floating_point.'"$$f"' meta "realized" "floating_point.'"$$f"'", "" end'; done; \
+	echo 'theory floating_point.'"$$f"' meta "realized_theory" "floating_point.'"$$f"'", "" end'; done; \
 	) > $@
 
 install_no_local::

src/core/ident.ml

@@ -158,9 +158,6 @@ let forget_all printer =
 
 (** Sanitizers *)
 
-let unsanitizable = Debug.register_info_flag "unsanitizable"
-  ~desc:"About@ the@ sanitazing@ during@ the@ pretty-printing."
-
 let char_to_alpha c = match c with
   | 'a'..'z' | 'A'..'Z' -> String.make 1 c
   | ' ' -> "sp" | '_'  -> "us" | '#' -> "sh"
@@ -177,10 +174,7 @@ let char_to_alpha c = match c with
   | '0' -> "zr" | '1'  -> "un" | '2' -> "du"
   | '3' -> "tr" | '4'  -> "qr" | '5' -> "qn"
   | '6' -> "sx" | '7'  -> "st" | '8' -> "oc"
-  | '9' -> "nn" | '\n' -> "br"
-  | _ ->
-    Debug.dprintf unsanitizable "Unsanitizable : '%c' can't be sanitized@." c;
-    "zz"
+  | '9' -> "nn" | '\n' -> "br" |  _  -> "zz"
 
 let char_to_lalpha c = String.uncapitalize (char_to_alpha c)
 let char_to_ualpha c = String.capitalize (char_to_alpha c)

src/core/printer.ml

@@ -49,7 +49,8 @@ let lookup_printer s =
 let list_printers () =
   Hstr.fold (fun k (desc,_) acc -> (k,desc)::acc) printers []
 
-let () = register_printer ~desc:"Print nothing" "(null)"
+let () = register_printer
+  ~desc:"Dummy@ printer@ with@ no@ output@ (used@ for@ debugging)." "(null)"
   (fun _ _ _ _ ?old:_ _ _ -> ())
 
 (** Syntax substitutions *)
@@ -191,27 +192,31 @@ let print_prelude_for_theory th fmt pm =
 exception KnownTypeSyntax of tysymbol
 exception KnownLogicSyntax of lsymbol
 
-let meta_syntax_type  = register_meta "syntax_type" [MTtysymbol; MTstring]
-  ~desc:"Specify@ the@ syntax@ used@ to@ pretty-print@ the@ type@ symbols.@ \
+let meta_syntax_type = register_meta "syntax_type" [MTtysymbol; MTstring]
+  ~desc:"Specify@ the@ syntax@ used@ to@ pretty-print@ a@ type@ symbol.@ \
          Can@ be@ specified@ in@ the@ driver@ with@ the@ 'syntax type'@ rule."
 
 let meta_syntax_logic = register_meta "syntax_logic" [MTlsymbol; MTstring]
-  ~desc:"Specify@ the@ syntax@ used@ to@ pretty-print@ the@ logic@ symbols.@ \
+  ~desc:"Specify@ the@ syntax@ used@ to@ pretty-print@ a@ function/predicate@ \
+         symbol.@ \
          Can@ be@ specified@ in@ the@ driver@ with@ the@ 'syntax function'@ \
-         rule."
+         or@ 'syntax predicate'@ rules."
 
-let meta_remove_prop  = register_meta "remove_prop" [MTprsymbol]
-  ~desc:"Specify@ the@ logical@ propositions@ to@ remove.@ \
-         Can@ be@ specified@ in@ the@ driver@ with@ the@ remove@ prop@ rule."
+let meta_remove_prop = register_meta "remove_prop" [MTprsymbol]
+  ~desc:"Remove@ a@ logical@ proposition@ from@ proof@ obligations.@ \
+         Can@ be@ specified@ in@ the@ driver@ with@ the@ 'remove prop'@ rule."
 
-let meta_remove_type_symbol  = register_meta "remove_type_symbol" [MTtysymbol]
-  ~desc:"Specify@ the@ type@ symbol@ to@ remove."
+let meta_remove_type = register_meta "remove_type" [MTtysymbol]
+  ~desc:"Remove@ a@ type@ symbol@ from@ proof@ obligations.@ \
+         Used@ in@ bisection."
 
-let meta_remove_logic  = register_meta "remove_logic" [MTlsymbol]
-  ~desc:"Specify@ the@ logic@ symbol@ propositions@ to@ remove."
+let meta_remove_logic = register_meta "remove_logic" [MTlsymbol]
+  ~desc:"Remove@ a@ function/predicate@ symbol@ from@ proof@ obligations.@ \
+         Used@ in@ bisection."
 
-let meta_realized     = register_meta "realized" [MTstring; MTstring]
-  ~desc:"TODO??"
+let meta_realized_theory = register_meta "realized_theory" [MTstring; MTstring]
+  ~desc:"Specify@ that@ a@ Why3@ theory@ is@ \"realized\"@ as@ a@ module@ \
+         in@ an@ ITP."
 
 let check_syntax_type ts s = check_syntax s (List.length ts.ts_args)
 

src/core/printer.mli

@@ -43,8 +43,8 @@ val meta_syntax_type : meta
 val meta_syntax_logic : meta
 val meta_remove_prop : meta
 val meta_remove_logic : meta
-val meta_remove_type_symbol : meta
-val meta_realized : meta
+val meta_remove_type : meta
+val meta_realized_theory : meta
 
 val syntax_type : tysymbol -> string -> tdecl
 val syntax_logic : lsymbol -> string -> tdecl

src/core/trans.ml

@@ -17,8 +17,7 @@ open Theory
 open Task
 
 let debug = Debug.register_info_flag "transform"
-  ~desc:"About@ which@ transformations@ are@ applied@ and@ with@ which@ \
-         arguments, ie metas."
+  ~desc:"Be@ verbose@ about@ application@ of@ proof@ task@ transformations."
 
 (** Task transformation *)
 

src/driver/autodetection.ml

@@ -46,7 +46,7 @@ module Wc = Whyconf
 open Rc
 
 let debug = Debug.register_info_flag "autodetect"
-  ~desc:"About@ the@ autodetection@ of@ external@ provers."
+  ~desc:"Be@ verbose@ about@ autodetection@ of@ external@ provers."
 
 (* auto-detection of provers *)
 

src/driver/call_provers.ml

@@ -113,11 +113,7 @@ let rec grep out l = match l with
 
 
 let debug = Debug.register_info_flag "call_prover"
-  ~desc:"About@ external@ prover@ calls@ and@ results."
-
-(*
-type res_waitpid = int * Unix.process_status
-*)
+  ~desc:"Be@ verbose@ about@ prover@ calls@ and@ keep@ temporary@ files."
 
 type post_prover_call = unit -> prover_result
 

src/ide/gconfig.ml

@@ -15,7 +15,8 @@ open Rc
 open Whyconf
 
 let debug = Debug.register_info_flag "ide_info"
-  ~desc:"About why3ide."
+  ~desc:"Print@ why3ide@ debugging@ messages."
+
 let () = Debug.set_flag debug
 
 (** set the exception call back handler to the Exn_printer of why3 *)

src/parser/glob.ml

@@ -11,8 +11,8 @@
 
 open Ident
 
-let flag = Debug.register_info_flag "glob"
-  ~desc:"TODO, used in parsing?"
+let flag = Debug.register_flag "track_use"
+  ~desc:"Track@ use/clone@ instructions.@ Used@ by@ why3doc."
 
 let () = Debug.unset_flag flag (* make sure it is unset by default *)
 

src/printer/coq.ml

@@ -836,7 +836,7 @@ let print_task env pr thpr _blacklist realize ?old fmt task =
   print_th_prelude task fmt thpr;
   (* find theories that are both used and realized from metas *)
   let realized_theories =
-    Task.on_meta meta_realized (fun mid args ->
+    Task.on_meta meta_realized_theory (fun mid args ->
       match args with
       | [Theory.MAstr s1; Theory.MAstr s2] ->
         (* TODO: do not split string; in fact, do not even use a string argument *)

src/printer/pvs.ml

@@ -820,7 +820,7 @@ let print_task env pr thpr _blacklist realize ?old fmt task =
   print_th_prelude task fmt thpr;
   (* find theories that are both used and realized from metas *)
   let realized_theories =
-    Task.on_meta meta_realized (fun mid args ->
+    Task.on_meta meta_realized_theory (fun mid args ->
       match args with
       | [Theory.MAstr s1; Theory.MAstr s2] ->
         let f,id =

src/transform/eliminate_definition.ml

@@ -42,9 +42,9 @@ let elim_abstract undef_ls rem_pr rem_ls rem_ts d = match d.d_node with
 
 let eliminate_builtin =
   Trans.on_tagged_ls Printer.meta_syntax_logic (fun undef_ls ->
-  Trans.on_tagged_pr Printer.meta_remove_prop  (fun rem_pr ->
-  Trans.on_tagged_ls Printer.meta_remove_logic  (fun rem_ls ->
-  Trans.on_tagged_ts Printer.meta_remove_type_symbol  (fun rem_ts ->
+  Trans.on_tagged_pr Printer.meta_remove_prop (fun rem_pr ->
+  Trans.on_tagged_ls Printer.meta_remove_logic (fun rem_ls ->
+  Trans.on_tagged_ts Printer.meta_remove_type (fun rem_ts ->
     Trans.decl (elim_abstract undef_ls rem_pr rem_ls rem_ts) None))))
 
 let () = Trans.register_transform "eliminate_builtin" eliminate_builtin
@@ -57,7 +57,7 @@ let compute_diff t1 t2 =
   let km = Mid.set_diff (Task.task_known t1) (Task.task_known t2) in
   let hdone = Hdecl.create 10 in
   let remove_ts acc ts =
-    (Printer.meta_remove_type_symbol, [Theory.MAts ts])::acc in
+    (Printer.meta_remove_type, [Theory.MAts ts])::acc in
   let remove_ls acc ls =
     (Printer.meta_remove_logic, [Theory.MAls ls])::acc in
   let remove_pr acc pr =
@@ -219,7 +219,7 @@ let _union_rem rem1 rem2 =
 
 let create_meta_rem_list rem =
   let remove_ts acc ts =
-    (Printer.meta_remove_type_symbol, [Theory.MAts ts])::acc in
+    (Printer.meta_remove_type, [Theory.MAts ts])::acc in
   let remove_ls acc ls =
     (Printer.meta_remove_logic, [Theory.MAls ls])::acc in
   let remove_pr acc pr =