Skip to content

Commit 6db7057

Browse files
fgdoraisfgdorais
committed
chore: remove deprecations
1 parent eac4e25 commit 6db7057

3 files changed

Lines changed: 0 additions & 298 deletions

File tree

‎UnicodeBasic/TableLookup.lean‎

Lines changed: 0 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -180,11 +180,6 @@ where
180180
@[inline]
181181
def lookupGC (c : UInt32) : GC := CLib.lookupProp c |>.toUInt32
182182

183-
set_option linter.deprecated false in
184-
@[inline, deprecated Unicode.lookupGC (since := "v1.3.0")]
185-
def lookupGeneralCategory (c : UInt32) : GeneralCategory :=
186-
.ofGC! (lookupGC c)
187-
188183
/-- Get name of a code point using lookup table
189184
190185
Unicode property: `Name` -/

‎UnicodeBasic/Types.lean‎

Lines changed: 0 additions & 265 deletions
Original file line numberDiff line numberDiff line change
@@ -492,271 +492,6 @@ def ofString! (s : Substring.Raw) : GC :=
492492

493493
end GC
494494

495-
set_option linter.deprecated false in
496-
@[deprecated Unicode.GC (since := "1.2.0")]
497-
structure GeneralCategory : Type where
498-
/-- Major general category of a code point -/
499-
major : MajorGeneralCategory
500-
/-- Minor general category of a code point -/
501-
minor : Option (MinorGeneralCategory major)
502-
deriving Inhabited, DecidableEq
503-
504-
set_option linter.deprecated false in section
505-
506-
/-- General category: letter (`L`) -/
507-
@[deprecated Unicode.GC.L (since := "1.2.0")]
508-
protected def GeneralCategory.L : GeneralCategory := ⟨.letter, none⟩
509-
/-- General category: cased letter (`LC`) -/
510-
@[deprecated Unicode.GC.LC (since := "1.2.0")]
511-
protected def GeneralCategory.LC : GeneralCategory := ⟨_, some .casedLetter⟩
512-
/-- General category: uppercase letter (`Lu`) -/
513-
@[deprecated Unicode.GC.Lu (since := "1.2.0")]
514-
protected def GeneralCategory.Lu : GeneralCategory := ⟨_, some .uppercaseLetter⟩
515-
/-- General category: lowercase letter (`Ll`) -/
516-
@[deprecated Unicode.GC.Ll (since := "1.2.0")]
517-
protected def GeneralCategory.Ll : GeneralCategory := ⟨_, some .lowercaseLetter⟩
518-
/-- General category: titlecase letter (`Lt`) -/
519-
@[deprecated Unicode.GC.Lt (since := "1.2.0")]
520-
protected def GeneralCategory.Lt : GeneralCategory := ⟨_, some .titlecaseLetter⟩
521-
/-- General category: modifier letter (`Lm`) -/
522-
@[deprecated Unicode.GC.Lm (since := "1.2.0")]
523-
protected def GeneralCategory.Lm : GeneralCategory := ⟨_, some .modifierLetter⟩
524-
/-- General category: other letter (`Lo`) -/
525-
@[deprecated Unicode.GC.Lo (since := "1.2.0")]
526-
protected def GeneralCategory.Lo : GeneralCategory := ⟨_, some .otherLetter⟩
527-
/-- General category mark (`M`) -/
528-
@[deprecated Unicode.GC.M (since := "1.2.0")]
529-
protected def GeneralCategory.M : GeneralCategory := ⟨.mark, none⟩
530-
/-- General category: nonspacing combining mark (`Mn`) -/
531-
@[deprecated Unicode.GC.Mn (since := "1.2.0")]
532-
protected def GeneralCategory.Mn : GeneralCategory := ⟨_, some .nonspacingMark⟩
533-
/-- General category: spacing combining mark (`Mc`) -/
534-
@[deprecated Unicode.GC.Mc (since := "1.2.0")]
535-
protected def GeneralCategory.Mc : GeneralCategory := ⟨_, some .spacingMark⟩
536-
/-- General category: enclosing combining mark (`Me`) -/
537-
@[deprecated Unicode.GC.Me (since := "1.2.0")]
538-
protected def GeneralCategory.Me : GeneralCategory := ⟨_, some .enclosingMark⟩
539-
/-- General category: number (`N`) -/
540-
@[deprecated Unicode.GC.N (since := "1.2.0")]
541-
protected def GeneralCategory.N : GeneralCategory := ⟨.number, none⟩
542-
/-- General category: decimal digit (`Nd`) -/
543-
@[deprecated Unicode.GC.Nd (since := "1.2.0")]
544-
protected def GeneralCategory.Nd : GeneralCategory := ⟨_, some .decimalNumber⟩
545-
/-- General category: letter number (`Nl`) -/
546-
@[deprecated Unicode.GC.Nl (since := "1.2.0")]
547-
protected def GeneralCategory.Nl : GeneralCategory := ⟨_, some .letterNumber⟩
548-
/-- General category: other number (`No`) -/
549-
@[deprecated Unicode.GC.No (since := "1.2.0")]
550-
protected def GeneralCategory.No : GeneralCategory := ⟨_, some .otherNumber⟩
551-
/-- General category: punctuation (`P`) -/
552-
@[deprecated Unicode.GC.P (since := "1.2.0")]
553-
protected def GeneralCategory.P : GeneralCategory := ⟨.punctuation, none⟩
554-
/-- General category: connector punctuation (`Pc`) -/
555-
@[deprecated Unicode.GC.Pc (since := "1.2.0")]
556-
protected def GeneralCategory.Pc : GeneralCategory := ⟨_, some .connectorPunctuation⟩
557-
/-- General category: dash punctuation (`Pd`) -/
558-
@[deprecated Unicode.GC.Pd (since := "1.2.0")]
559-
protected def GeneralCategory.Pd : GeneralCategory := ⟨_, some .dashPunctuation⟩
560-
/-- General category: grouping punctuation (`PG`) -/
561-
@[deprecated Unicode.GC.PG (since := "1.2.0")]
562-
protected def GeneralCategory.PG : GeneralCategory := ⟨_, some .groupPunctuation⟩
563-
/-- General category: opening punctuation (`Ps`) -/
564-
@[deprecated Unicode.GC.Ps (since := "1.2.0")]
565-
protected def GeneralCategory.Ps : GeneralCategory := ⟨_, some .openPunctuation⟩
566-
/-- General category: closing punctuation (`Pe`) -/
567-
@[deprecated Unicode.GC.Pe (since := "1.2.0")]
568-
protected def GeneralCategory.Pe : GeneralCategory := ⟨_, some .closePunctuation⟩
569-
/-- General category: quoting punctuation (`PQ`) -/
570-
@[deprecated Unicode.GC.PQ (since := "1.2.0")]
571-
protected def GeneralCategory.PQ : GeneralCategory := ⟨_, some .quotePunctuation⟩
572-
/-- General category: initial punctuation (`Pi`) -/
573-
@[deprecated Unicode.GC.Pi (since := "1.2.0")]
574-
protected def GeneralCategory.Pi : GeneralCategory := ⟨_, some .initialPunctuation⟩
575-
/-- General category: final punctuation (`Pf`) -/
576-
@[deprecated Unicode.GC.Pf (since := "1.2.0")]
577-
protected def GeneralCategory.Pf : GeneralCategory := ⟨_, some .finalPunctuation⟩
578-
/-- General category: other punctuation (`Po`) -/
579-
@[deprecated Unicode.GC.Po (since := "1.2.0")]
580-
protected def GeneralCategory.Po : GeneralCategory := ⟨_, some .otherPunctuation⟩
581-
/-- General category: symbol (`S`) -/
582-
@[deprecated Unicode.GC.S (since := "1.2.0")]
583-
protected def GeneralCategory.S : GeneralCategory := ⟨.symbol, none⟩
584-
/-- General category: math symbol (`Sm`) -/
585-
@[deprecated Unicode.GC.Sm (since := "1.2.0")]
586-
protected def GeneralCategory.Sm : GeneralCategory := ⟨_, some .mathSymbol⟩
587-
/-- General category: currency symbol (`Sc`) -/
588-
@[deprecated Unicode.GC.Sc (since := "1.2.0")]
589-
protected def GeneralCategory.Sc : GeneralCategory := ⟨_, some .currencySymbol⟩
590-
/-- General category: modifier symbol (`Sk`) -/
591-
@[deprecated Unicode.GC.Sk (since := "1.2.0")]
592-
protected def GeneralCategory.Sk : GeneralCategory := ⟨_, some .modifierSymbol⟩
593-
/-- General category: other symbol (`So`) -/
594-
@[deprecated Unicode.GC.So (since := "1.2.0")]
595-
protected def GeneralCategory.So : GeneralCategory := ⟨_, some .otherSymbol⟩
596-
/-- General category: separator (`Z`) -/
597-
@[deprecated Unicode.GC.Z (since := "1.2.0")]
598-
protected def GeneralCategory.Z : GeneralCategory := ⟨.separator, none⟩
599-
/-- General category: space separator (`Zs`) -/
600-
@[deprecated Unicode.GC.Zs (since := "1.2.0")]
601-
protected def GeneralCategory.Zs : GeneralCategory := ⟨_, some .spaceSeparator⟩
602-
/-- General category: line separator (`Zl`) -/
603-
@[deprecated Unicode.GC.Zl (since := "1.2.0")]
604-
protected def GeneralCategory.Zl : GeneralCategory := ⟨_, some .lineSeparator⟩
605-
/-- General category: paragraph separator (`Zp`) -/
606-
@[deprecated Unicode.GC.Zp (since := "1.2.0")]
607-
protected def GeneralCategory.Zp : GeneralCategory := ⟨_, some .paragraphSeparator⟩
608-
/-- General category: other (`C`) -/
609-
@[deprecated Unicode.GC.C (since := "1.2.0")]
610-
protected def GeneralCategory.C : GeneralCategory := ⟨.other, none⟩
611-
/-- General category: control (`Cc`) -/
612-
@[deprecated Unicode.GC.Cc (since := "1.2.0")]
613-
protected def GeneralCategory.Cc : GeneralCategory := ⟨_, some .control⟩
614-
/-- General category: format (`Cf`) -/
615-
@[deprecated Unicode.GC.Cf (since := "1.2.0")]
616-
protected def GeneralCategory.Cf : GeneralCategory := ⟨_, some .format⟩
617-
/-- General category: surrogate (`Cs`) -/
618-
@[deprecated Unicode.GC.Cs (since := "1.2.0")]
619-
protected def GeneralCategory.Cs : GeneralCategory := ⟨_, some .surrogate⟩
620-
/-- General category: private use (`Co`) -/
621-
@[deprecated Unicode.GC.Co (since := "1.2.0")]
622-
protected def GeneralCategory.Co : GeneralCategory := ⟨_, some .privateUse⟩
623-
/-- General category: unassigned (`Cn`) -/
624-
@[deprecated Unicode.GC.Cn (since := "1.2.0")]
625-
protected def GeneralCategory.Cn : GeneralCategory := ⟨_, some .unassigned⟩
626-
627-
/-- String abbreviation for general category -/
628-
@[deprecated Unicode.GC.toAbbrev! (since := "1.2.0")]
629-
def GeneralCategory.toAbbrev : GeneralCategory → String
630-
| ⟨.letter, none⟩ => "L"
631-
| ⟨_, some .casedLetter⟩ => "LC"
632-
| ⟨_, some .uppercaseLetter⟩ => "Lu"
633-
| ⟨_, some .lowercaseLetter⟩ => "Ll"
634-
| ⟨_, some .titlecaseLetter⟩ => "Lt"
635-
| ⟨_, some .modifierLetter⟩ => "Lm"
636-
| ⟨_, some .otherLetter⟩ => "Lo"
637-
| ⟨.mark, none⟩ => "M"
638-
| ⟨_, some .nonspacingMark⟩ => "Mn"
639-
| ⟨_, some .spacingMark⟩ => "Mc"
640-
| ⟨_, some .enclosingMark⟩ => "Me"
641-
| ⟨.number, none⟩ => "N"
642-
| ⟨_, some .decimalNumber⟩ => "Nd"
643-
| ⟨_, some .letterNumber⟩ => "Nl"
644-
| ⟨_, some .otherNumber⟩ => "No"
645-
| ⟨.punctuation, none⟩ => "P"
646-
| ⟨_, some .connectorPunctuation⟩ => "Pc"
647-
| ⟨_, some .dashPunctuation⟩ => "Pd"
648-
| ⟨_, some .groupPunctuation⟩ => "PG"
649-
| ⟨_, some .openPunctuation⟩ => "Ps"
650-
| ⟨_, some .closePunctuation⟩ => "Pe"
651-
| ⟨_, some .quotePunctuation⟩ => "PQ"
652-
| ⟨_, some .initialPunctuation⟩ => "Pi"
653-
| ⟨_, some .finalPunctuation⟩ => "Pf"
654-
| ⟨_, some .otherPunctuation⟩ => "Po"
655-
| ⟨.symbol, none⟩ => "S"
656-
| ⟨_, some .mathSymbol⟩ => "Sm"
657-
| ⟨_, some .currencySymbol⟩ => "Sc"
658-
| ⟨_, some .modifierSymbol⟩ => "Sk"
659-
| ⟨_, some .otherSymbol⟩ => "So"
660-
| ⟨.separator, none⟩ => "Z"
661-
| ⟨_, some .spaceSeparator⟩ => "Zs"
662-
| ⟨_, some .lineSeparator⟩ => "Zl"
663-
| ⟨_, some .paragraphSeparator⟩ => "Zp"
664-
| ⟨.other, none⟩ => "C"
665-
| ⟨_, some .control⟩ => "Cc"
666-
| ⟨_, some .format⟩ => "Cf"
667-
| ⟨_, some .surrogate⟩ => "Cs"
668-
| ⟨_, some .privateUse⟩ => "Co"
669-
| ⟨_, some .unassigned⟩ => "Cn"
670-
671-
/-- Get general category from string abbreviation -/
672-
@[deprecated Unicode.GC.ofAbbrev? (since := "1.2.0")]
673-
def GeneralCategory.ofAbbrev? (s : Substring.Raw) : Option GeneralCategory :=
674-
if s.bsize = 0 || s.bsize > 2 then none else
675-
match s.get 0 with
676-
| 'C' =>
677-
if s.bsize = 1 then some ⟨.other, none⟩ else
678-
match s.get ⟨1⟩ with
679-
| 'c' => some ⟨_, some .control⟩
680-
| 'f' => some ⟨_, some .format⟩
681-
| 's' => some ⟨_, some .surrogate⟩
682-
| 'o' => some ⟨_, some .privateUse⟩
683-
| 'n' => some ⟨_, some .unassigned⟩
684-
| _ => none
685-
| 'L' =>
686-
if s.bsize = 1 then some ⟨.letter, none⟩ else
687-
match s.get ⟨1⟩ with
688-
| 'C' => some ⟨_, some .casedLetter⟩
689-
| 'u' => some ⟨_, some .uppercaseLetter⟩
690-
| 'l' => some ⟨_, some .lowercaseLetter⟩
691-
| 't' => some ⟨_, some .titlecaseLetter⟩
692-
| 'm' => some ⟨_, some .modifierLetter⟩
693-
| 'o' => some ⟨_, some .otherLetter⟩
694-
| _ => none
695-
| 'M' =>
696-
if s.bsize = 1 then some ⟨.mark, none⟩ else
697-
match s.get ⟨1⟩ with
698-
| 'n' => some ⟨_, some .nonspacingMark⟩
699-
| 'c' => some ⟨_, some .spacingMark⟩
700-
| 'e' => some ⟨_, some .enclosingMark⟩
701-
| _ => none
702-
| 'N' =>
703-
if s.bsize = 1 then some ⟨.number, none⟩ else
704-
match s.get ⟨1⟩ with
705-
| 'd' => some ⟨_, some .decimalNumber⟩
706-
| 'l' => some ⟨_, some .letterNumber⟩
707-
| 'o' => some ⟨_, some .otherNumber⟩
708-
| _ => none
709-
| 'P' =>
710-
if s.bsize = 1 then some ⟨.punctuation, none⟩ else
711-
match s.get ⟨1⟩ with
712-
| 'G' => some ⟨_, some .groupPunctuation⟩
713-
| 'Q' => some ⟨_, some .quotePunctuation⟩
714-
| 'c' => some ⟨_, some .connectorPunctuation⟩
715-
| 'd' => some ⟨_, some .dashPunctuation⟩
716-
| 's' => some ⟨_, some .openPunctuation⟩
717-
| 'e' => some ⟨_, some .closePunctuation⟩
718-
| 'i' => some ⟨_, some .initialPunctuation⟩
719-
| 'f' => some ⟨_, some .finalPunctuation⟩
720-
| 'o' => some ⟨_, some .otherPunctuation⟩
721-
| _ => none
722-
| 'S' =>
723-
if s.bsize = 1 then some ⟨.symbol, none⟩ else
724-
match s.get ⟨1⟩ with
725-
| 'm' => some ⟨_, some .mathSymbol⟩
726-
| 'c' => some ⟨_, some .currencySymbol⟩
727-
| 'k' => some ⟨_, some .modifierSymbol⟩
728-
| 'o' => some ⟨_, some .otherSymbol⟩
729-
| _ => none
730-
| 'Z' =>
731-
if s.bsize = 1 then some ⟨.separator, none⟩ else
732-
match s.get ⟨1⟩ with
733-
| 's' => some ⟨_, some .spaceSeparator⟩
734-
| 'l' => some ⟨_, some .lineSeparator⟩
735-
| 'p' => some ⟨_, some .paragraphSeparator⟩
736-
| _ => none
737-
| _ => none
738-
739-
@[deprecated Unicode.GC.ofAbbrev! (since := "1.2.0"), inherit_doc GeneralCategory.ofAbbrev?]
740-
def GeneralCategory.ofAbbrev! (s : Substring) : GeneralCategory :=
741-
match ofAbbrev? s with
742-
| some gc => gc
743-
| none => panic! "invalid general category abbreviation"
744-
745-
instance : Repr GeneralCategory where
746-
reprPrec gc _ := s!"Unicode.GeneralCategory.{gc.toAbbrev}"
747-
748-
@[deprecated some (since := "1.2.0")]
749-
def GeneralCategory.ofGC? (c : GC) : Option GeneralCategory :=
750-
match GC.reprAux c with
751-
| [a] => GeneralCategory.ofAbbrev! a
752-
| _ => none
753-
754-
@[deprecated id (since := "1.2.0")]
755-
def GeneralCategory.ofGC! (c : GC) : GeneralCategory :=
756-
(ofGC? c).get!
757-
758-
end
759-
760495
/-!
761496
## Numeric Type and Value ##
762497
-/

‎UnicodeData/Basic.lean‎

Lines changed: 0 additions & 28 deletions
Original file line numberDiff line numberDiff line change
@@ -35,34 +35,6 @@ structure UnicodeData where
3535
titlecase : Option Char := none
3636
deriving BEq, Repr
3737

38-
@[deprecated UnicodeData.code (since := "1.2.0")]
39-
abbrev UnicodeData.codeValue := @UnicodeData.code
40-
41-
@[deprecated UnicodeData.name (since := "1.2.0")]
42-
abbrev UnicodeData.characterName := @UnicodeData.name
43-
44-
set_option linter.deprecated false in
45-
@[deprecated UnicodeData.gc (since := "1.2.0")]
46-
def UnicodeData.generalCategory (d : UnicodeData) : GeneralCategory := .ofGC! d.gc
47-
48-
@[deprecated UnicodeData.bidi (since := "1.2.0")]
49-
abbrev UnicodeData.bidiClass := @UnicodeData.bidi
50-
51-
@[deprecated UnicodeData.cc (since := "1.2.0")]
52-
abbrev UnicodeData.canonicalCombiningClass := @UnicodeData.cc
53-
54-
@[deprecated UnicodeData.cc (since := "1.2.0")]
55-
abbrev UnicodeData.decompositionMapping := @UnicodeData.decomp
56-
57-
@[deprecated UnicodeData.lowercase (since := "1.2.0")]
58-
abbrev UnicodeData.lowercaseMapping := @UnicodeData.lowercase
59-
60-
@[deprecated UnicodeData.uppercase (since := "1.2.0")]
61-
abbrev UnicodeData.uppercaseMapping := @UnicodeData.uppercase
62-
63-
@[deprecated UnicodeData.titlecase (since := "1.2.0")]
64-
abbrev UnicodeData.titlecaseMapping := @UnicodeData.titlecase
65-
6638
instance : Inhabited UnicodeData where
6739
default := {
6840
code := 0

0 commit comments

Comments
 (0)