Skip to content
Browse files

Fixing ml-doc.

  • Loading branch information...
1 parent f3b3b6e commit c7b9eebd6e754672d0d57ea6a376bd3d7abf0159 @ppedrot ppedrot committed May 1, 2014
Showing with 49 additions and 61 deletions.
  1. +3 −3 Makefile.build
  2. +1 −1 ide/sentence.ml
  3. +9 −14 kernel/nativecode.ml
  4. +6 −9 lib/serialize.ml
  5. +3 −3 library/declaremods.ml
  6. +3 −3 plugins/micromega/coq_micromega.ml
  7. +6 −6 plugins/micromega/mfourier.ml
  8. +18 −22 stm/stm.ml
View
6 Makefile.build
@@ -707,13 +707,13 @@ $(OCAMLDOCDIR)/coq.tex: $(DOCMLIS:.mli=.cmi)
-intro $(OCAMLDOCDIR)/docintro -o $@
mli-doc: $(DOCMLIS:.mli=.cmi)
- $(OCAMLDOC) -html -rectypes -I $(MYCAMLP4LIB) $(MLINCLUDES)\
+ $(OCAMLDOC) -html -rectypes -I +threads -I $(MYCAMLP4LIB) $(MLINCLUDES) $(COQIDEFLAGS)\
$(DOCMLIS) -d $(OCAMLDOCDIR)/html -colorize-code \
-t "Coq mlis documentation" -intro $(OCAMLDOCDIR)/docintro \
-css-style style.css
ml-dot: $(MLFILES)
- $(OCAMLDOC) -dot -dot-reduce -rectypes -I $(CAMLLIB) -I $(MYCAMLP4LIB) $(MLINCLUDES)\
+ $(OCAMLDOC) -dot -dot-reduce -rectypes -I +threads -I $(CAMLLIB) -I $(MYCAMLP4LIB) $(MLINCLUDES) $(COQIDEFLAGS)\
$(filter $(addsuffix /%.ml,$(CORESRCDIRS)),$(MLFILES)) -o $(OCAMLDOCDIR)/coq.dot
%_dep.png: %.dot
@@ -729,7 +729,7 @@ OCAMLDOC_MLLIBD = $(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ \
$(OCAMLDOC_MLLIBD)
ml-doc:
- $(OCAMLDOC) -html -rectypes $(LOCALINCLUDES) -d $(SOURCEDOCDIR) $(MLSTATICFILES)
+ $(OCAMLDOC) -html -rectypes -I +threads $(MLINCLUDES) $(COQIDEFLAGS) -d $(OCAMLDOCDIR) $(MLSTATICFILES)
parsing/parsing.dot : | parsing/parsing.mllib.d parsing/highparsing.mllib.d
$(OCAMLDOC_MLLIBD)
View
2 ide/sentence.ml
@@ -67,7 +67,7 @@ let rec grab_sentence_stop (start:GText.iter) =
(forward_search is_sentence_end start)#forward_char
(** Search forward the first character immediately after a "." sentence end
- (and not just a "{" or "}" or comment end *)
+ (and not just a "\{" or "\}" or comment end *)
let rec grab_ending_dot (start:GText.iter) =
let is_ending_dot s = is_sentence_end s && s#char = Char.code '.' in
View
23 kernel/nativecode.ml
@@ -21,7 +21,7 @@ open Pre_env
compiler. mllambda represents a fragment of ML, and can easily be printed
to OCaml code. *)
-(** Local names {{{**)
+(** Local names **)
type lname = { lname : name; luid : int }
@@ -42,9 +42,8 @@ let reset_lname = lname_ctr := -1
let fresh_lname n =
incr lname_ctr;
{ lname = n; luid = !lname_ctr }
- (**}}}**)
-(** Global names {{{ **)
+(** Global names **)
type gname =
| Gind of string * inductive (* prefix, inductive name *)
| Gconstruct of string * constructor (* prefix, constructor name *)
@@ -136,9 +135,8 @@ let reset_normtbl () = normtbl_ctr := -1
let fresh_gnormtbl l =
incr normtbl_ctr;
Gnormtbl (l,!normtbl_ctr)
- (**}}}**)
-(** Symbols (pre-computed values) {{{**)
+(** Symbols (pre-computed values) **)
type symbol =
| SymbValue of Nativevalues.t
@@ -241,9 +239,9 @@ let symbols_tbl_name = Ginternal "symbols_tbl"
let get_symbols_tbl () =
let tbl = Array.make (HashtblSymbol.length symb_tbl) dummy_symb in
- HashtblSymbol.iter (fun x i -> tbl.(i) <- x) symb_tbl; tbl(**}}}**)
+ HashtblSymbol.iter (fun x i -> tbl.(i) <- x) symb_tbl; tbl
-(** Lambda to Mllambda {{{**)
+(** Lambda to Mllambda **)
type primitive =
| Mk_prod
@@ -1250,9 +1248,8 @@ let mllambda_of_lambda auxdefs l t =
(* final result : global list, fv, ml *)
else
(!global_stack, (fv_named, fv_rel), mkMLlam (Array.of_list params) ml)
- (**}}}**)
-(** Code optimization {{{**)
+(** Code optimization **)
(** Optimization of match and fix *)
@@ -1408,9 +1405,8 @@ let optimize_stk stk =
Glet(Gconstant (prefix, c), optimize gdef body)
| _ -> g in
List.map optimize_global stk
- (**}}}**)
-(** Printing to ocaml {{{**)
+(** Printing to ocaml **)
(* Redefine a bunch of functions in module Names to generate names
acceptable to OCaml. *)
let string_of_id s = Unicode.ascii_of_ident (string_of_id s)
@@ -1708,9 +1704,9 @@ let pp_global fmt g =
pp_gname gn pp_ldecls params
pp_mllam (MLmatch(annot,a,accu,bs))
| Gcomment s ->
- Format.fprintf fmt "@[(* %s *)@]@." s(**}}}**)
+ Format.fprintf fmt "@[(* %s *)@]@." s
-(** Compilation of elements in environment {{{**)
+(** Compilation of elements in environment **)
let rec compile_with_fv env sigma auxdefs l t =
let (auxdefs,(fv_named,fv_rel),ml) = mllambda_of_lambda auxdefs l t in
if List.is_empty fv_named && List.is_empty fv_rel then (auxdefs,ml)
@@ -1961,6 +1957,5 @@ let update_locations (ind_updates,const_updates) =
let add_header_comment mlcode s =
Gcomment s :: mlcode
-(** }}} **)
(* vim: set filetype=ocaml foldmethod=marker: *)
View
15 lib/serialize.ml
@@ -19,7 +19,7 @@ open Interface
open Xml_datatype
(* Marshalling of basic types and type constructors *)
-module Xml_marshalling = struct (* {{{ *)
+module Xml_marshalling = struct
exception Marshal_error
@@ -370,12 +370,12 @@ let to_feedback xml = match xml with
content = to_feedback_content content }
| _ -> raise Marshal_error
-end (* }}} *)
+end
include Xml_marshalling
(* Reification of basic types and type constructors, and functions
from to xml *)
-module ReifType : sig (* {{{ *)
+module ReifType : sig
type 'a val_t
@@ -609,7 +609,7 @@ end = struct
(pr_xml (of_option_state { opt_sync = true; opt_depr = false;
opt_name = "name1"; opt_value = IntValue (Some 37) }));
-end (* }}} *)
+end
open ReifType
(** Types reification, checked with explicit casts *)
@@ -755,7 +755,7 @@ let abstract_eval_call handler (c : 'a call) : 'a value =
with any ->
Fail (handler.handle_exn any)
-(** brain dead code, edit if protocol messages are added/removed {{{ *)
+(** brain dead code, edit if protocol messages are added/removed *)
let of_answer (q : 'a call) (v : 'a value) : xml = match q with
| Add _ -> of_value (of_value_type add_rty_t ) (Obj.magic v)
| Edit_at _ -> of_value (of_value_type edit_at_rty_t ) (Obj.magic v)
@@ -833,15 +833,14 @@ let to_call : xml -> unknown call =
| "Interp" -> Interp (mkCallArg interp_sty_t a)
| "StopWorker" -> StopWorker (mkCallArg stop_worker_sty_t a)
| _ -> raise Marshal_error)
-(* }}} *)
(** misc *)
let is_feedback = function
| Element ("feedback", _, _) -> true
| _ -> false
-(** {{{ Debug printing *)
+(** Debug printing *)
let pr_value_gen pr = function
| Good v -> "GOOD " ^ pr v
@@ -885,8 +884,6 @@ let pr_call call = match call with
| Interp x -> str_of_call call ^ " " ^ print interp_sty_t x
| StopWorker x -> str_of_call call ^ " " ^ print stop_worker_sty_t x
-(* }}} *)
-
let document to_string_fmt =
Printf.printf "=== Available calls ===\n\n";
Array.iter (fun (cname, csty, crty) ->
View
6 library/declaremods.ml
@@ -332,7 +332,7 @@ let () = ModSubstObjs.set_missing_handler handle_missing_substobjs
-(** {6 From module expression to substitutive objects *)
+(** {6 From module expression to substitutive objects} *)
(** Turn a chain of [MSEapply] into the head module_path and the
list of module_path parameters (deepest param coming first).
@@ -668,7 +668,7 @@ let declare_module interp_modast id args res mexpr_o fs =
end
-(** {6 Module types : start, end, declare *)
+(** {6 Module types : start, end, declare} *)
module RawModTypeOps = struct
@@ -787,7 +787,7 @@ let declare_include interp me_asts =
end
-(** {6 Module operations handling summary freeze/unfreeze *)
+(** {6 Module operations handling summary freeze/unfreeze} *)
let protect_summaries f =
let fs = Summary.freeze_summaries ~marshallable:`No in
View
6 plugins/micromega/coq_micromega.ml
@@ -45,7 +45,7 @@ type tag = Tag.t
(**
* An atom is of the form:
- * pExpr1 {<,>,=,<>,<=,>=} pExpr2
+ * pExpr1 \{<,>,=,<>,<=,>=\} pExpr2
* where pExpr1, pExpr2 are polynomial expressions (see Micromega). pExprs are
* parametrized by 'cst, which is used as the type of constants.
*)
@@ -112,7 +112,7 @@ let rec ids_of_formula f =
(**
* A clause is a list of (tagged) nFormulas.
* nFormulas are normalized formulas, i.e., of the form:
- * cPol {=,<>,>,>=} 0
+ * cPol \{=,<>,>,>=\} 0
* with cPol compact polynomials (see the Pol inductive type in EnvRing.v).
*)
@@ -246,7 +246,7 @@ let rec add_term t0 = function
module ISet = Set.Make(Int)
(**
- * Given a set of integers s={i0,...,iN} and a list m, return the list of
+ * Given a set of integers s=\{i0,...,iN\} and a list m, return the list of
* elements of m that are at position i0,...,iN.
*)
View
12 plugins/micromega/mfourier.ml
@@ -19,10 +19,10 @@ struct
type interval = num option * num option
(** None models the absence of bound i.e. infinity *)
(** As a result,
- - None , None -> ]-oo,+oo[
- - None , Some v -> ]-oo,v]
- - Some v, None -> [v,+oo[
- - Some v, Some v' -> [v,v']
+ - None , None -> \]-oo,+oo\[
+ - None , Some v -> \]-oo,v\]
+ - Some v, None -> \[v,+oo\[
+ - Some v, Some v' -> \[v,v'\]
Intervals needs to be explicitely normalised.
*)
@@ -117,7 +117,7 @@ and cstr_info = {
}
-(** A system of constraints has the form [{sys = s ; vars = v}].
+(** A system of constraints has the form [\{sys = s ; vars = v\}].
[s] is a hashtable mapping a normalised vector to a [cstr_info] record where
- [bound] is an interval
- [prf_idx] is the set of hypothese indexes (i.e. constraints in the initial system) used to obtain the current constraint.
@@ -499,7 +499,7 @@ let pick_small_value bnd =
then ceiling_num i (* why not *) else i
-(** [solution s1 sys_l = Some(sn,[(vn-1,sn-1);...; (v1,s1)]@sys_l)]
+(** [solution s1 sys_l = Some(sn,\[(vn-1,sn-1);...; (v1,s1)\]\@sys_l)]
then [sn] is a system which contains only [black_v] -- if it existed in [s1]
and [sn+1] is obtained by projecting [vn] out of [sn]
@raise SystemContradiction if system [s] has no solution
View
40 stm/stm.ml
@@ -130,7 +130,7 @@ module Vcs_aux : sig
exception Expired
val visit : (branch_type, transaction,'i) Vcs_.t -> Vcs_.Dag.node -> visit
-end = struct (* {{{ *)
+end = struct
let proof_nesting vcs =
List.fold_left max 0
@@ -171,7 +171,7 @@ end = struct (* {{{ *)
| _ -> anomaly (str ("Malformed VCS at node "^Stateid.to_string id))
with Not_found -> raise Expired
-end (* }}} *)
+end
(* Imperative wrap around VCS to obtain _the_ VCS *)
module VCS : sig
@@ -234,15 +234,15 @@ module VCS : sig
val backup : unit -> vcs
val restore : vcs -> unit
-end = struct (* {{{ *)
+end = struct
include Vcs_
exception Expired = Vcs_aux.Expired
module StateidSet = Set.Make(Stateid)
open Printf
- let print_dag vcs () = (* {{{ *)
+ let print_dag vcs () =
let fname = "stm_" ^ process_id () in
let string_of_transaction = function
| Cmd (t, _) | Fork (t, _,_,_) ->
@@ -325,8 +325,7 @@ end = struct (* {{{ *)
close_out oc;
ignore(Sys.command
("dot -Tpdf -Gcharset=latin1 " ^ fname_dot ^ " -o" ^ fname_ps))
- (* }}} *)
-
+
type vcs = (branch_type, transaction, vcs state_info) t
let vcs : vcs ref = ref (empty Stateid.dummy)
@@ -454,7 +453,7 @@ end = struct (* {{{ *)
val command : now:bool -> (unit -> unit) -> unit
- end = struct (* {{{ *)
+ end = struct
let m = Mutex.create ()
let c = Condition.create ()
@@ -486,15 +485,15 @@ end = struct (* {{{ *)
worker := Some (Thread.create run_command ())
end
- end (* }}} *)
+ end
let print ?(now=false) () =
if not !Flags.debug && not now then () else NB.command ~now (print_dag !vcs)
let backup () = !vcs
let restore v = vcs := v
-end (* }}} *)
+end
(* Fills in the nodes of the VCS *)
module State : sig
@@ -517,7 +516,7 @@ module State : sig
val get_cached : Stateid.t -> frozen_state
val assign : Stateid.t -> frozen_state -> unit
-end = struct (* {{{ *)
+end = struct
(* cur_id holds Stateid.dummy in case the last attempt to define a state
* failed, so the global state may contain garbage *)
@@ -600,7 +599,6 @@ end = struct (* {{{ *)
| None -> raise (exn_on id ~valid:good_id e)
end
-(* }}} *)
let hints = ref Aux_file.empty_aux_file
let set_compilation_hints file =
@@ -670,7 +668,7 @@ module Slaves : sig
val set_perspective : Stateid.t list -> unit
-end = struct (* {{{ *)
+end = struct
let cancel_worker n = WorkersPool.cancel (n-1)
@@ -1152,15 +1150,15 @@ end = struct (* {{{ *)
List.map (function ReqBuildProof(a,b,c,d,x,e) ->
ReqBuildProof(a,b,c,d,List.assoc x f2t_map,e)) tasks
-end (* }}} *)
+end
(* Runs all transactions needed to reach a state *)
module Reach : sig
val known_state :
?redefine_qed:bool -> cache:Summary.marshallable -> Stateid.t -> unit
-end = struct (* {{{ *)
+end = struct
let pstate = ["meta counter"; "evar counter"; "program-tcc-table"]
@@ -1366,7 +1364,8 @@ let known_state ?(redefine_qed=false) ~cache id =
prerr_endline ("reached: "^ Stateid.to_string id) in
reach ~redefine_qed id
-end (* }}} *)
+end
+
let _ = Slaves.set_reach_known_state Reach.known_state
(* The backtrack module simulates the classic behavior of a linear document *)
@@ -1382,7 +1381,7 @@ module Backtrack : sig
(* To be installed during initialization *)
val undo_vernac_classifier : vernac_expr -> vernac_classification
-end = struct (* {{{ *)
+end = struct
let record () =
let current_branch = VCS.current_branch () in
@@ -1497,7 +1496,7 @@ end = struct (* {{{ *)
msg_warning(str"undo_vernac_classifier: going back to the initial state.");
VtStm (VtBack Stateid.initial, true), VtNow
-end (* }}} *)
+end
let init () =
VCS.init Stateid.initial;
@@ -1806,7 +1805,7 @@ let process_transaction ~tty verbose c (loc, expr) =
let e = Errors.push e in
handle_failure e vcs tty
-(** STM interface {{{******************************************************* **)
+(** STM interface ******************************************************* **)
let stop_worker n = Slaves.cancel_worker n
@@ -1945,9 +1944,8 @@ let edit_at id =
VCS.restore vcs;
VCS.print ();
raise e
-(* }}} *)
-(** Old tty interface {{{*************************************************** **)
+(** Old tty interface *************************************************** **)
let interp verb (_,e as lexpr) =
let clas = classify_vernac e in
@@ -2070,6 +2068,4 @@ let show_script ?proof () =
msg_notice (v 0 (Pp.prlist_with_sep Pp.fnl (fun x -> x) indented_cmds))
with Vcs_aux.Expired -> ()
-(* }}} *)
-
(* vim:set foldmethod=marker: *)

0 comments on commit c7b9eeb

Please sign in to comment.
Something went wrong with that request. Please try again.