package coq-core
The Coq Proof Assistant -- Core Binaries and Tools
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.20.0.tar.gz
md5=66e57ea55275903bef74d5bf36fbe0f1
sha512=1a7eac6e2f58724a3f9d68bbb321e4cfe963ba1a5551b9b011db4b3f559c79be433d810ff262593d753770ee41ea68fbd6a60daa1e2319ea00dff64c8851d70b
doc/src/coq-core.toplevel/workerLoop.ml.html
Source file workerLoop.ml
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43
(************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) (* v * Copyright INRIA, CNRS and contributors *) (* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (* * (see LICENSE file for the text of the license) *) (************************************************************************) let kind_filter str = let kinds = [ "--kind=proof"; "--kind=tactic"; "--kind=query" ] in not (List.exists (String.equal str) kinds) let worker_parse_extra extra_args = let stm_opts, extra_args = Stmargs.parse_args ~init:Stm.AsyncOpts.default_opts extra_args in let extra_args = List.filter kind_filter extra_args in ((),stm_opts), extra_args let worker_init init ((),stm_opts) injections ~opts : Vernac.State.t = Flags.quiet := true; init (); Coqtop.init_toploop opts stm_opts injections let usage = Boot.Usage.{ executable_name = "coqworker"; extra_args = ""; extra_options = ("\n" ^ "coqworker" ^ " specific options:\ \n --xml_format=Ppcmds serialize pretty printing messages using the std_ppcmds format\n"); } let start ~init ~loop = let open Coqtop in let custom = { parse_extra = worker_parse_extra; usage; initial_args = Coqargs.default; init_extra = worker_init init; run = (fun ((),_) ~opts:_ (_state : Vernac.State.t) -> (* the state is not used since the worker will receive one from master *) loop ()); } in start_coq custom
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>