package dedukti
An implementation of The Lambda-Pi Modulo Theory
Install
Dune Dependency
Authors
Maintainers
Sources
v2.7.tar.gz
sha512=97171b48dd96043d84587581d72edb442f63e7b5ac1695771aa1c3c9074739e15bc7d17678fedb7062acbf403a0bf323d97485c31b92376b80c63b5c2300ee3c
sha256=5e1b6a859dfa1eb2098947a99c7d11ee450f750d96da1720f4834e1505d1096c
doc/src/dedukti.parsers/parser.ml.html
Source file parser.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
open Kernel open Basic type stream = {md : Basic.mident; lexbuf : Lexing.lexbuf} type from = Channel of in_channel | String of string (* String of Dedukti code *) type input = {file : string option; md : Basic.mident; from : from} exception Parse_error of loc * string let read str = try Menhir_parser.line Lexer.token str.lexbuf str.md with Menhir_parser.Error -> let loc = Lexer.get_loc str.lexbuf in let lex = Lexing.lexeme str.lexbuf in let msg = Format.sprintf "Unexpected token '%s'." lex in raise @@ Parse_error (loc, msg) let lexing_from input = match input with | String s -> Lexing.from_string s | Channel ic -> Lexing.from_channel ic let md_of_file file = let open Filename in let base = basename file in let base = if check_suffix base ".dk" then chop_suffix base ".dk" else base in mk_mident base let input_from_file file = let md = md_of_file file in let from = Channel (open_in file) in {file = Some file; from; md} let input_from_stdin md = {file = None; from = Channel stdin; md} let input_from_string md s = {file = None; from = String s; md} let md_of_input t = t.md let file_of_input t = t.file let close input = match input.from with String _ -> () | Channel ic -> close_in ic let from input = let md = input.md in {md; lexbuf = lexing_from input.from} let handle input f = let s = from input in try while true do f (read s) done with Parsing.Parse_error | End_of_file -> () let parse input = let l = ref [] in handle input (fun e -> l := e :: !l); List.rev !l
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>