package coq
Formal proof management system
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.15.1.tar.gz
sha256=513e953b7183d478acb75fd6e80e4dc32ac1a918cf4343ac31a859cfb4e9aad2
doc/src/coq-core.printing/ppextend.ml.html
Source file ppextend.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 116 117 118 119 120 121 122 123 124
(************************************************************************) (* * 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) *) (************************************************************************) open Util open Pp open CErrors open Notation open Constrexpr (*s Pretty-print. *) type ppbox = | PpHB | PpHOVB of int | PpHVB of int | PpVB of int type ppcut = | PpBrk of int * int | PpFnl let ppcmd_of_box = function | PpHB -> h | PpHOVB n -> hov n | PpHVB n -> hv n | PpVB n -> v n let ppcmd_of_cut = function | PpFnl -> fnl () | PpBrk(n1,n2) -> brk(n1,n2) type pattern_quote_style = QuotedPattern | NotQuotedPattern type unparsing = | UnpMetaVar of entry_relative_level * Extend.side option | UnpBinderMetaVar of entry_relative_level * pattern_quote_style | UnpListMetaVar of entry_relative_level * unparsing list * Extend.side option | UnpBinderListMetaVar of bool * unparsing list | UnpTerminal of string | UnpBox of ppbox * unparsing Loc.located list | UnpCut of ppcut type unparsing_rule = unparsing list type extra_unparsing_rules = (string * string) list let rec unparsing_eq unp1 unp2 = match (unp1,unp2) with | UnpMetaVar (p1,s1), UnpMetaVar (p2,s2) -> entry_relative_level_eq p1 p2 && s1 = s2 | UnpBinderMetaVar (p1,s1), UnpBinderMetaVar (p2,s2) -> entry_relative_level_eq p1 p2 && s1 = s2 | UnpListMetaVar (p1,l1,s1), UnpListMetaVar (p2,l2,s2) -> entry_relative_level_eq p1 p2 && List.for_all2eq unparsing_eq l1 l2 && s1 = s2 | UnpBinderListMetaVar (b1,l1), UnpBinderListMetaVar (b2,l2) -> b1 = b2 && List.for_all2eq unparsing_eq l1 l2 | UnpTerminal s1, UnpTerminal s2 -> String.equal s1 s2 | UnpBox (b1,l1), UnpBox (b2,l2) -> b1 = b2 && List.for_all2eq unparsing_eq (List.map snd l1) (List.map snd l2) | UnpCut p1, UnpCut p2 -> p1 = p2 | (UnpMetaVar _ | UnpBinderMetaVar _ | UnpListMetaVar _ | UnpBinderListMetaVar _ | UnpTerminal _ | UnpBox _ | UnpCut _), _ -> false (* Register generic and specific printing rules *) type notation_printing_rules = { notation_printing_unparsing : unparsing_rule; notation_printing_level : entry_level; notation_printing_extra : extra_unparsing_rules; } type generic_notation_printing_rules = { notation_printing_reserved : bool; notation_printing_rules : notation_printing_rules; } let generic_notation_printing_rules = Summary.ref ~name:"generic-notation-printing-rules" (NotationMap.empty : generic_notation_printing_rules NotationMap.t) let specific_notation_printing_rules = Summary.ref ~name:"specific-notation-printing-rules" (SpecificNotationMap.empty : notation_printing_rules SpecificNotationMap.t) let declare_generic_notation_printing_rules ntn rules = generic_notation_printing_rules := NotationMap.add ntn rules !generic_notation_printing_rules let declare_specific_notation_printing_rules specific_ntn rules = specific_notation_printing_rules := SpecificNotationMap.add specific_ntn rules !specific_notation_printing_rules let has_generic_notation_printing_rule ntn = try (NotationMap.find ntn !generic_notation_printing_rules).notation_printing_reserved with Not_found -> false let find_generic_notation_printing_rule ntn = NotationMap.find ntn !generic_notation_printing_rules let find_specific_notation_printing_rule specific_ntn = SpecificNotationMap.find specific_ntn !specific_notation_printing_rules let find_notation_printing_rule which ntn = try match which with | None -> raise Not_found (* Normally not the case *) | Some which -> (find_specific_notation_printing_rule (which,ntn)) with Not_found -> (find_generic_notation_printing_rule ntn).notation_printing_rules let find_notation_extra_printing_rules which ntn = try match which with | None -> raise Not_found | Some which -> (find_specific_notation_printing_rule (which,ntn)).notation_printing_extra with Not_found -> (find_generic_notation_printing_rule ntn).notation_printing_rules.notation_printing_extra let add_notation_extra_printing_rule ntn k v = try generic_notation_printing_rules := let { notation_printing_reserved; notation_printing_rules } = NotationMap.find ntn !generic_notation_printing_rules in let rules = { notation_printing_reserved; notation_printing_rules = { notation_printing_rules with notation_printing_extra = (k,v) :: notation_printing_rules.notation_printing_extra } } in NotationMap.add ntn rules !generic_notation_printing_rules with Not_found -> user_err (str "No such Notation.")
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>