From c7b9eebd6e754672d0d57ea6a376bd3d7abf0159 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 1 May 2014 02:31:55 +0200 Subject: Fixing ml-doc. --- Makefile.build | 6 +++--- ide/sentence.ml | 2 +- kernel/nativecode.ml | 23 +++++++++------------- lib/serialize.ml | 15 ++++++-------- library/declaremods.ml | 6 +++--- plugins/micromega/coq_micromega.ml | 6 +++--- plugins/micromega/mfourier.ml | 12 ++++++------ stm/stm.ml | 40 +++++++++++++++++--------------------- 8 files changed, 49 insertions(+), 61 deletions(-) diff --git a/Makefile.build b/Makefile.build index dd7b20f0f..db2d0f720 100644 --- a/Makefile.build +++ b/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) diff --git a/ide/sentence.ml b/ide/sentence.ml index 9c361c81f..557a86b2b 100644 --- a/ide/sentence.ml +++ b/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 diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index f38a2c314..1f6effba6 100644 --- a/kernel/nativecode.ml +++ b/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: *) diff --git a/lib/serialize.ml b/lib/serialize.ml index c97817779..042b75e2d 100644 --- a/lib/serialize.ml +++ b/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,7 +833,6 @@ 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 *) @@ -841,7 +840,7 @@ 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) -> diff --git a/library/declaremods.ml b/library/declaremods.ml index bb623b7a1..e4f227637 100644 --- a/library/declaremods.ml +++ b/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 diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index db998f32b..9515c5de9 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/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. *) diff --git a/plugins/micromega/mfourier.ml b/plugins/micromega/mfourier.ml index a6c2e0a59..050bd310d 100644 --- a/plugins/micromega/mfourier.ml +++ b/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 diff --git a/stm/stm.ml b/stm/stm.ml index e791e37cf..6fe3fd03a 100644 --- a/stm/stm.ml +++ b/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,7 +234,7 @@ module VCS : sig val backup : unit -> vcs val restore : vcs -> unit -end = struct (* {{{ *) +end = struct include Vcs_ exception Expired = Vcs_aux.Expired @@ -242,7 +242,7 @@ end = struct (* {{{ *) 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,7 +485,7 @@ 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) @@ -494,7 +493,7 @@ end = struct (* {{{ *) 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,7 +1150,7 @@ 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 @@ -1160,7 +1158,7 @@ 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: *) -- cgit v1.2.3