package vscoq-language-server
VSCoq language server
Install
Dune Dependency
Authors
Maintainers
Sources
vscoq-language-server-2.1.7.tar.gz
md5=81c195fcbe9b23c26db9704a0b8e37f8
sha512=9b175796b231e3663b1cdd546fde898c1d19a6a4eb16671970797045e0e29acc008630634f0d15fa34a94ccc14a0c16d3851efbf0b74f3e1ac6ada1f1461f7e1
doc/src/vscoq-language-server.dm/log.ml.html
Source file log.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 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115
(**************************************************************************) (* *) (* VSCoq *) (* *) (* Copyright INRIA and contributors *) (* (see version control and README file for authors & dates) *) (* *) (**************************************************************************) (* *) (* This file is distributed under the terms of the MIT License. *) (* See LICENSE file. *) (* *) (**************************************************************************) open Types let lsp_initialization_done = ref false let initialization_feedback_queue = Queue.create () let init_log = try Some ( let oc = open_out @@ Filename.temp_file "vscoq_init_log." ".txt" in output_string oc "command line:\n"; output_string oc (String.concat " " (Sys.argv |> Array.to_list)); output_string oc "\nstatic initialization:\n"; oc) with _ -> None let write_to_init_log str = Option.iter (fun oc -> output_string oc str; output_char oc '\n'; flush oc) init_log let rec is_enabled name = function | [] -> false | "-vscoq-d" :: "all" :: _ -> true | "-vscoq-d" :: v :: rest -> List.mem name (String.split_on_char ',' v) || is_enabled name rest | _ :: rest -> is_enabled name rest let logs = ref [] let handle_event s = Printf.eprintf "%s\n" s let mk_log name = logs := name :: !logs; let flag = is_enabled name (Array.to_list Sys.argv) in let flag_init = is_enabled "init" (Array.to_list Sys.argv) in write_to_init_log ("log " ^ name ^ " is " ^ if flag then "on" else "off"); Log (fun msg -> let should_print_log = flag || (flag_init && not !lsp_initialization_done) in if should_print_log then begin let txt = Format.asprintf "[%-20s, %d, %f] %s" name (Unix.getpid ()) (Unix.gettimeofday ()) msg in if not !lsp_initialization_done then begin write_to_init_log txt; Queue.push txt initialization_feedback_queue (* Emission must be delayed as per LSP spec *) end else handle_event txt end else ()) let logs () = List.sort String.compare !logs type event = string type events = event Sel.Event.t list [%% if coq = "8.18" || coq = "8.19" || coq = "8.20"] let feedback_add_feeder_on_Message f = Feedback.add_feeder (fun fb -> match fb.Feedback.contents with | Feedback.Message(a,b,c) -> f fb.Feedback.route fb.Feedback.span_id fb.Feedback.doc_id a b [] c | _ -> ()) [%%else] let feedback_add_feeder_on_Message f = Feedback.add_feeder (fun fb -> match fb.Feedback.contents with | Feedback.Message(a,b,c,d) -> f fb.Feedback.route fb.Feedback.span_id fb.Feedback.doc_id a b c d | _ -> ()) [%%endif] let install_debug_feedback f = feedback_add_feeder_on_Message (fun _route _span _doc lvl loc _qf m -> match lvl, loc with | Feedback.Debug,None -> f Pp.(string_of_ppcmds m) | _ -> ()) (* We go through a queue in case we receive a debug feedback from Coq before we replied to Initialize *) let coq_debug_feedback_queue = Queue.create () let main_debug_feeder = install_debug_feedback (fun txt -> Queue.push txt coq_debug_feedback_queue) let debug : event Sel.Event.t = Sel.On.queue ~name:"debug" ~priority:PriorityManager.feedback coq_debug_feedback_queue (fun x -> x) let cancel_debug_event = Sel.Event.get_cancellation_handle debug let lsp_initialization_done () = lsp_initialization_done := true; Option.iter close_out_noerr init_log; Queue.iter handle_event initialization_feedback_queue; Queue.clear initialization_feedback_queue; [debug] let worker_initialization_begins () = Sel.Event.cancel cancel_debug_event; Feedback.del_feeder main_debug_feeder; (* We do not want to inherit master's Feedback reader (feeder), otherwise we would output on the worker's stderr. Debug feedback from worker is forwarded to master via a specific handler (see [worker_initialization_done]) *) Queue.clear coq_debug_feedback_queue let worker_initialization_done ~fwd_event = let _ = install_debug_feedback fwd_event in ()
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>