- options : Lean.Options
- table : Lean.Parser.TokenTable
- stxTrav : Lean.Syntax.Traverser
- leadWord : String
- isUngrouped : Bool
- mustBeGrouped : Bool
- stack : Array Lean.Format
@[inline]
@[inline]
def
Lean.PrettyPrinter.FormatterM.orElse
{α : Type}
(p₁ : Lean.PrettyPrinter.FormatterM α)
(p₂ : Unit → Lean.PrettyPrinter.FormatterM α)
:
Equations
- Lean.PrettyPrinter.FormatterM.orElse p₁ p₂ = do let s ← get Lean.catchInternalId Lean.PrettyPrinter.backtrackExceptionId p₁ fun x => do set s p₂ ()
Equations
- Lean.PrettyPrinter.instOrElseFormatterM = { orElse := Lean.PrettyPrinter.FormatterM.orElse }
@[inline]
Equations
- Lean.PrettyPrinter.mkFormatterAttribute = Lean.KeyedDeclsAttribute.init { builtinName := `builtinFormatter, name := `formatter, descr := "Register a formatter for a parser.\n\n [formatter k] registers a declaration of type `Lean.PrettyPrinter.Formatter` for the `SyntaxNodeKind` `k`.", valueTypeName := `Lean.PrettyPrinter.Formatter, evalKey := fun builtin stx => do let env ← Lean.getEnv let id ← Lean.Attribute.Builtin.getId stx if (builtin && Option.isSome (Lean.Environment.find? env id) || Lean.Parser.isValidSyntaxNodeKind env id) = true then pure id else Lean.throwError (Lean.toMessageData "invalid [formatter] argument, unknown syntax kind '" ++ Lean.toMessageData id ++ Lean.toMessageData "'"), onAdded := fun builtin declName => pure () } `Lean.PrettyPrinter.formatterAttribute
Equations
- Lean.PrettyPrinter.mkCombinatorFormatterAttribute = Lean.ParserCompiler.registerCombinatorAttribute `combinatorFormatter "Register a formatter for a parser combinator.\n\n [combinatorFormatter c] registers a declaration of type `Lean.PrettyPrinter.Formatter` for the `Parser` declaration `c`.\n Note that, unlike with [formatter], this is not a node kind since combinators usually do not introduce their own node kinds.\n The tagged declaration may optionally accept parameters corresponding to (a prefix of) those of `c`, where `Parser` is replaced\n with `Formatter` in the parameter types."
Equations
- Lean.PrettyPrinter.Formatter.throwBacktrack = throw (Lean.Exception.internal Lean.PrettyPrinter.backtrackExceptionId)
Equations
- Lean.PrettyPrinter.Formatter.instMonadTraverserFormatterM = { st := { get := Lean.PrettyPrinter.Formatter.State.stxTrav <$> get, set := fun t => modify fun st => { stxTrav := t, leadWord := st.leadWord, isUngrouped := st.isUngrouped, mustBeGrouped := st.mustBeGrouped, stack := st.stack }, modifyGet := fun {α} f => modifyGet fun st => let x := f st.stxTrav; match x with | (a, t) => (a, { stxTrav := t, leadWord := st.leadWord, isUngrouped := st.isUngrouped, mustBeGrouped := st.mustBeGrouped, stack := st.stack }) } }
Equations
- Lean.PrettyPrinter.Formatter.getStack = do let st ← get pure st.stack
Equations
- Lean.PrettyPrinter.Formatter.getStackSize = do let stack ← Lean.PrettyPrinter.Formatter.getStack pure (Array.size stack)
Equations
- Lean.PrettyPrinter.Formatter.setStack stack = modify fun st => { stxTrav := st.stxTrav, leadWord := st.leadWord, isUngrouped := st.isUngrouped, mustBeGrouped := st.mustBeGrouped, stack := stack }
Equations
- Lean.PrettyPrinter.Formatter.pushWhitespace f = do Lean.PrettyPrinter.Formatter.push f modify fun st => { stxTrav := st.stxTrav, leadWord := "", isUngrouped := false, mustBeGrouped := st.mustBeGrouped, stack := st.stack }
Equations
- Lean.PrettyPrinter.Formatter.visitArgs x = do let stx ← Lean.Syntax.MonadTraverser.getCur let _do_jp : Unit → Lean.PrettyPrinter.FormatterM Unit := fun y => Lean.Syntax.MonadTraverser.goLeft if Array.size (Lean.Syntax.getArgs stx) > 0 then do let y ← SeqLeft.seqLeft (SeqRight.seqRight (Lean.Syntax.MonadTraverser.goDown (Array.size (Lean.Syntax.getArgs stx) - 1)) fun x => x) fun x => Lean.Syntax.MonadTraverser.goUp _do_jp y else do let y ← pure PUnit.unit _do_jp y
def
Lean.PrettyPrinter.Formatter.fold
(fn : Array Lean.Format → Lean.Format)
(x : Lean.PrettyPrinter.FormatterM Unit)
:
Equations
- Lean.PrettyPrinter.Formatter.fold fn x = do let sp ← Lean.PrettyPrinter.Formatter.getStackSize x let stack ← Lean.PrettyPrinter.Formatter.getStack let f : Lean.Format := fn (Array.extract stack sp (Array.size stack)) Lean.PrettyPrinter.Formatter.setStack (Array.push (Array.shrink stack sp) f)
Equations
- Lean.PrettyPrinter.Formatter.concat x = Lean.PrettyPrinter.Formatter.fold (fun as => Array.foldl (fun acc f => if Std.Format.isNil acc = true then f else f ++ acc) Lean.Format.nil as 0 (Array.size as)) x
def
Lean.PrettyPrinter.Formatter.indent
(x : Lean.PrettyPrinter.Formatter)
(indent : optParam (Option Int) none)
:
Equations
- Lean.PrettyPrinter.Formatter.indent x indent = do Lean.PrettyPrinter.Formatter.concat x let ctx ← read let indent : Int := Option.getD indent (Int.ofNat (Std.Format.getIndent ctx.options)) modify fun st => { stxTrav := st.stxTrav, leadWord := st.leadWord, isUngrouped := st.isUngrouped, mustBeGrouped := st.mustBeGrouped, stack := Array.modify st.stack (Array.size st.stack - 1) (Lean.Format.nest indent) }
Equations
- Lean.PrettyPrinter.Formatter.fill x = do Lean.PrettyPrinter.Formatter.concat x modify fun st => { stxTrav := st.stxTrav, leadWord := st.leadWord, isUngrouped := false, mustBeGrouped := st.mustBeGrouped, stack := Array.modify st.stack (Array.size st.stack - 1) Lean.Format.fill }
Equations
- Lean.PrettyPrinter.Formatter.group x = do Lean.PrettyPrinter.Formatter.concat x modify fun st => { stxTrav := st.stxTrav, leadWord := st.leadWord, isUngrouped := false, mustBeGrouped := st.mustBeGrouped, stack := Array.modify st.stack (Array.size st.stack - 1) fun a => Lean.Format.group a }
def
Lean.PrettyPrinter.Formatter.withMaybeTag
(pos? : Option String.Pos)
(x : Lean.PrettyPrinter.FormatterM Unit)
:
Equations
- Lean.PrettyPrinter.Formatter.withMaybeTag pos? x = match pos? with | some p => do Lean.PrettyPrinter.Formatter.concat x modify fun st => { stxTrav := st.stxTrav, leadWord := st.leadWord, isUngrouped := st.isUngrouped, mustBeGrouped := st.mustBeGrouped, stack := Array.modify st.stack (Array.size st.stack - 1) (Lean.Format.tag p) } | x => x
def
Lean.PrettyPrinter.Formatter.orelse.formatter
(p1 : Lean.PrettyPrinter.Formatter)
(p2 : Lean.PrettyPrinter.Formatter)
:
Equations
- Lean.PrettyPrinter.Formatter.orelse.formatter p1 p2 = HOrElse.hOrElse p1 fun x => p2
@[extern lean_mk_antiquot_formatter]
constant
Lean.PrettyPrinter.Formatter.mkAntiquot.formatter'
(name : String)
(kind : Option Lean.SyntaxNodeKind)
(anonymous : optParam Bool true)
:
@[extern lean_pretty_printer_formatter_interpret_parser_descr]
Equations
-
Lean.PrettyPrinter.Formatter.formatterForKindUnsafe k = if (k == `missing) = true then do
Lean.PrettyPrinter.Formatter.push (Std.Format.text "
" ) Lean.Syntax.MonadTraverser.goLeft else do let stx ← Lean.Syntax.MonadTraverser.getCur let f ← liftM (Lean.PrettyPrinter.runForNodeKind Lean.PrettyPrinter.formatterAttribute k Lean.PrettyPrinter.Formatter.interpretParserDescr') Lean.PrettyPrinter.Formatter.withMaybeTag (Lean.PrettyPrinter.Formatter.getExprPos? stx) f
@[implementedBy Lean.PrettyPrinter.Formatter.formatterForKindUnsafe]
def
Lean.PrettyPrinter.Formatter.withAntiquotSuffixSplice.formatter
(k : Lean.SyntaxNodeKind)
(p : Lean.PrettyPrinter.Formatter)
(suffix : Lean.PrettyPrinter.Formatter)
:
Equations
- Lean.PrettyPrinter.Formatter.withAntiquotSuffixSplice.formatter k p suffix = do let a ← Lean.Syntax.MonadTraverser.getCur if Lean.Syntax.isAntiquotSuffixSplice a = true then Lean.PrettyPrinter.Formatter.visitArgs (SeqRight.seqRight suffix fun x => p) else p
Equations
- Lean.PrettyPrinter.Formatter.tokenWithAntiquot.formatter p = do let a ← Lean.Syntax.MonadTraverser.getCur if Lean.Syntax.isTokenAntiquot a = true then Lean.PrettyPrinter.Formatter.visitArgs p else p
Equations
- Lean.PrettyPrinter.Formatter.categoryFormatterCore cat = do modify fun st => { stxTrav := st.stxTrav, leadWord := st.leadWord, isUngrouped := false, mustBeGrouped := true, stack := st.stack } let stx ← Lean.Syntax.MonadTraverser.getCur let cls : Lean.Name := `PrettyPrinter.format let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.PrettyPrinter.FormatterM Unit := fun y => let _do_jp := fun y => modify fun st => { stxTrav := st.stxTrav, leadWord := st.leadWord, isUngrouped := !st.mustBeGrouped, mustBeGrouped := true, stack := st.stack }; if (Lean.Syntax.getKind stx == `choice) = true then do let y ← Lean.PrettyPrinter.Formatter.visitArgs do let a ← Lean.Syntax.MonadTraverser.getCur Lean.PrettyPrinter.Formatter.formatterForKind (Lean.Syntax.getKind a) _do_jp y else do let y ← Lean.PrettyPrinter.Formatter.withAntiquot.formatter (Lean.PrettyPrinter.Formatter.mkAntiquot.formatter' (Lean.Name.toString cat) none true) (Lean.PrettyPrinter.Formatter.formatterForKind (Lean.Syntax.getKind stx)) _do_jp y if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "formatting " ++ Lean.toMessageData (Lean.indentD (Lean.MessageData.ofFormat (Lean.format stx))) ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y
Equations
- Lean.PrettyPrinter.Formatter.categoryParser.formatter cat = do Lean.PrettyPrinter.Formatter.concat (Lean.PrettyPrinter.Formatter.categoryFormatterCore cat) let a ← get if a.isUngrouped = true then pure PUnit.unit else do let a ← read let indent : Nat := Std.Format.getIndent a.options modify fun st => { stxTrav := st.stxTrav, leadWord := st.leadWord, isUngrouped := st.isUngrouped, mustBeGrouped := st.mustBeGrouped, stack := Array.modify st.stack (Array.size st.stack - 1) fun fmt => Lean.Format.fill (Lean.Format.nest (Int.ofNat indent) fmt) }
Equations
- Lean.PrettyPrinter.Formatter.categoryParserOfStack.formatter offset = do let st ← get let stx : Lean.Syntax := Lean.Syntax.getArg (Array.back st.stxTrav.parents) (Array.back st.stxTrav.idxs - offset) Lean.PrettyPrinter.Formatter.categoryParser.formatter (Lean.Syntax.getId stx)
Equations
- Lean.PrettyPrinter.Formatter.parserOfStack.formatter offset prec = do let st ← get let stx : Lean.Syntax := Lean.Syntax.getArg (Array.back st.stxTrav.parents) (Array.back st.stxTrav.idxs - offset) Lean.PrettyPrinter.Formatter.formatterForKind (Lean.Syntax.getKind stx)
Equations
Equations
def
Lean.PrettyPrinter.Formatter.andthen.formatter
(p1 : Lean.PrettyPrinter.Formatter)
(p2 : Lean.PrettyPrinter.Formatter)
:
Equations
- Lean.PrettyPrinter.Formatter.andthen.formatter p1 p2 = SeqRight.seqRight p2 fun x => p1
Equations
- Lean.PrettyPrinter.Formatter.checkKind k = do let stx ← Lean.Syntax.MonadTraverser.getCur if (k != Lean.Syntax.getKind stx) = true then let cls := `PrettyPrinter.format.backtrack; do let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.PrettyPrinter.FormatterM Unit := fun y => Lean.PrettyPrinter.Formatter.throwBacktrack if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "unexpected node kind '" ++ Lean.toMessageData (Lean.Syntax.getKind stx) ++ Lean.toMessageData "', expected '" ++ Lean.toMessageData k ++ Lean.toMessageData "'") _do_jp y else do let y ← pure PUnit.unit _do_jp y else pure PUnit.unit
Equations
- Lean.PrettyPrinter.Formatter.parseToken s = do let a ← Lean.getEnv let a_1 ← Lean.getOptions let a_2 ← read pure (Lean.Parser.andthenFn Lean.Parser.whitespace (Lean.Parser.tokenFn []) { toInputContext := { input := s, fileName := "", fileMap := Lean.FileMap.ofString "" }, toParserModuleContext := { env := a, options := a_1, currNamespace := Lean.Name.anonymous, openDecls := [] }, prec := 0, tokens := a_2.table, quotDepth := 0, suppressInsideQuot := false, savedPos? := none, forbiddenTk? := none } (Lean.Parser.mkParserState s))
Equations
- Lean.PrettyPrinter.Formatter.pushToken info tk = let _do_jp := fun y => do let st ← get let _do_jp : PUnit → Lean.PrettyPrinter.FormatterM Unit := fun y => match info with | Lean.SourceInfo.original ss x x_1 x_2 => let ss' := Substring.trim ss; if (!Substring.isEmpty ss') = true then let ws := { str := ss.str, startPos := ss'.stopPos, stopPos := ss.stopPos }; let _do_jp := fun y => modify fun st => { stxTrav := st.stxTrav, leadWord := "", isUngrouped := st.isUngrouped, mustBeGrouped := st.mustBeGrouped, stack := st.stack }; if Substring.contains ws (Char.ofNat 10) = true then do let a ← Lean.getOptions let y ← Lean.PrettyPrinter.Formatter.indent (Lean.PrettyPrinter.Formatter.push (Std.Format.text (toString "" ++ toString ss' ++ toString "\n"))) (some (0 - Int.ofNat (Std.Format.getIndent a))) _do_jp y else do Lean.PrettyPrinter.Formatter.pushLine let y ← Lean.PrettyPrinter.Formatter.push (Std.Format.text (Substring.toString ss')) _do_jp y else pure PUnit.unit | x => pure () if (st.leadWord != "" && String.trimRight tk == tk) = true then let tk' := String.trimLeft tk; do let t ← Lean.PrettyPrinter.Formatter.parseToken (tk' ++ st.leadWord) if t.pos ≤ String.bsize tk' then do Lean.PrettyPrinter.Formatter.push (Std.Format.text tk) let y ← modify fun st => { stxTrav := st.stxTrav, leadWord := if (String.trimLeft tk == tk) = true then tk ++ st.leadWord else "", isUngrouped := st.isUngrouped, mustBeGrouped := st.mustBeGrouped, stack := st.stack } _do_jp y else do Lean.PrettyPrinter.Formatter.push (Std.Format.text tk ++ Std.Format.text " ") let y ← modify fun st => { stxTrav := st.stxTrav, leadWord := if (String.trimLeft tk == tk) = true then tk else "", isUngrouped := st.isUngrouped, mustBeGrouped := st.mustBeGrouped, stack := st.stack } _do_jp y else let _do_jp := fun y => do let y ← modify fun st => { stxTrav := st.stxTrav, leadWord := if (String.trimLeft tk == tk) = true then tk else "", isUngrouped := st.isUngrouped, mustBeGrouped := st.mustBeGrouped, stack := st.stack } _do_jp y; if (st.leadWord == "") = true then do let y ← Lean.PrettyPrinter.Formatter.push (Std.Format.text (String.trimRight tk)) _do_jp y else if String.endsWith tk " " = true then do Lean.PrettyPrinter.Formatter.pushLine let y ← Lean.PrettyPrinter.Formatter.push (Std.Format.text (String.trimRight tk)) _do_jp y else do let y ← Lean.PrettyPrinter.Formatter.push (Std.Format.text tk) _do_jp y; match info with | Lean.SourceInfo.original x x_1 ss x_2 => let ss' := Substring.trim ss; if (!Substring.isEmpty ss') = true then let ws := { str := ss.str, startPos := ss'.stopPos, stopPos := ss.stopPos }; let _do_jp := fun y => do let y ← modify fun st => { stxTrav := st.stxTrav, leadWord := "", isUngrouped := st.isUngrouped, mustBeGrouped := st.mustBeGrouped, stack := st.stack } _do_jp y; if Substring.contains ws (Char.ofNat 10) = true then do let y ← Lean.PrettyPrinter.Formatter.push (Std.Format.text (toString "\n" ++ toString ss' ++ toString "")) _do_jp y else do let y ← Lean.PrettyPrinter.Formatter.push (Std.Format.text (toString " " ++ toString ss' ++ toString "")) _do_jp y else do let y ← pure PUnit.unit _do_jp y | x => do let y ← pure () _do_jp y
Equations
- Lean.PrettyPrinter.Formatter.symbolNoAntiquot.formatter sym = do let stx ← Lean.Syntax.MonadTraverser.getCur if Lean.Syntax.isToken sym stx = true then do let discr ← pure stx match discr with | Lean.Syntax.atom info x => do Lean.PrettyPrinter.Formatter.withMaybeTag (Lean.PrettyPrinter.Formatter.getExprPos? stx) (Lean.PrettyPrinter.Formatter.pushToken info sym) Lean.Syntax.MonadTraverser.goLeft | x => panicWithPosWithDecl "Lean.PrettyPrinter.Formatter" "Lean.PrettyPrinter.Formatter.symbolNoAntiquot.formatter" 369 42 "unreachable code has been reached" else let cls := `PrettyPrinter.format.backtrack; do let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.PrettyPrinter.FormatterM Unit := fun y => Lean.PrettyPrinter.Formatter.throwBacktrack if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "unexpected syntax '" ++ Lean.toMessageData (Lean.format stx) ++ Lean.toMessageData "', expected symbol '" ++ Lean.toMessageData sym ++ Lean.toMessageData "'") _do_jp y else do let y ← pure PUnit.unit _do_jp y
def
Lean.PrettyPrinter.Formatter.unicodeSymbolNoAntiquot.formatter
(sym : String)
(asciiSym : String)
:
Equations
- Lean.PrettyPrinter.Formatter.unicodeSymbolNoAntiquot.formatter sym asciiSym = do let a ← Lean.Syntax.MonadTraverser.getCur let discr ← Lean.Syntax.MonadTraverser.getCur match discr with | Lean.Syntax.atom info val => let _do_jp := fun y => Lean.Syntax.MonadTraverser.goLeft; if (val == String.trim sym) = true then do let y ← Lean.PrettyPrinter.Formatter.pushToken info sym _do_jp y else do let y ← Lean.PrettyPrinter.Formatter.pushToken info asciiSym _do_jp y | x => Lean.throwError (Lean.toMessageData "not an atom: " ++ Lean.toMessageData a ++ Lean.toMessageData "")
Equations
- Lean.PrettyPrinter.Formatter.identNoAntiquot.formatter = do Lean.PrettyPrinter.Formatter.checkKind Lean.identKind let a ← Lean.Syntax.MonadTraverser.getCur let discr ← Lean.Syntax.MonadTraverser.getCur match discr with | Lean.Syntax.ident info x id x_1 => let id := Lean.Name.simpMacroScopes id; do Lean.PrettyPrinter.Formatter.pushToken info (Lean.Name.toString id) Lean.Syntax.MonadTraverser.goLeft | x => Lean.throwError (Lean.toMessageData "not an ident: " ++ Lean.toMessageData a ++ Lean.toMessageData "")
Equations
- Lean.PrettyPrinter.Formatter.rawIdentNoAntiquot.formatter = do Lean.PrettyPrinter.Formatter.checkKind Lean.identKind let a ← Lean.Syntax.MonadTraverser.getCur let discr ← Lean.Syntax.MonadTraverser.getCur match discr with | Lean.Syntax.ident info x id x_1 => do Lean.PrettyPrinter.Formatter.pushToken info (Lean.Name.toString id) Lean.Syntax.MonadTraverser.goLeft | x => Lean.throwError (Lean.toMessageData "not an ident: " ++ Lean.toMessageData a ++ Lean.toMessageData "")
Equations
- Lean.PrettyPrinter.Formatter.visitAtom k = do let stx ← Lean.Syntax.MonadTraverser.getCur let _do_jp : Unit → Lean.PrettyPrinter.FormatterM Unit := fun y => do let discr ← pure (Lean.Syntax.ifNode stx (fun n => Lean.SyntaxNode.getArg n 0) fun x => stx) match discr with | Lean.Syntax.atom info val => do Lean.PrettyPrinter.Formatter.pushToken info val Lean.Syntax.MonadTraverser.goLeft | x => Lean.throwError (Lean.toMessageData "not an atom: " ++ Lean.toMessageData stx ++ Lean.toMessageData "") if (k != Lean.Name.anonymous) = true then do let y ← Lean.PrettyPrinter.Formatter.checkKind k _do_jp y else do let y ← pure PUnit.unit _do_jp y
Equations
- Lean.PrettyPrinter.Formatter.manyNoAntiquot.formatter p = do let stx ← Lean.Syntax.MonadTraverser.getCur Lean.PrettyPrinter.Formatter.visitArgs (Nat.forM (Array.size (Lean.Syntax.getArgs stx)) fun x => p)
Equations
- Lean.PrettyPrinter.Formatter.many1Unbox.formatter p = do let stx ← Lean.Syntax.MonadTraverser.getCur if (Lean.Syntax.getKind stx == Lean.nullKind) = true then Lean.PrettyPrinter.Formatter.manyNoAntiquot.formatter p else p
def
Lean.PrettyPrinter.Formatter.sepByNoAntiquot.formatter
(p : Lean.PrettyPrinter.Formatter)
(pSep : Lean.PrettyPrinter.Formatter)
:
Equations
- Lean.PrettyPrinter.Formatter.sepByNoAntiquot.formatter p pSep = do let stx ← Lean.Syntax.MonadTraverser.getCur Lean.PrettyPrinter.Formatter.visitArgs (List.forM (List.reverse (List.range (Array.size (Lean.Syntax.getArgs stx)))) fun i => if (i % 2 == 0) = true then p else pSep)
def
Lean.PrettyPrinter.Formatter.setExpected.formatter
(expected : List String)
(p : Lean.PrettyPrinter.Formatter)
:
Equations
- Lean.PrettyPrinter.Formatter.setExpected.formatter expected p = p
def
Lean.PrettyPrinter.Formatter.evalInsideQuot.formatter
(declName : Lean.Name)
(p : Lean.PrettyPrinter.Formatter)
:
Equations
- Lean.PrettyPrinter.Formatter.evalInsideQuot.formatter declName p = p
Equations
- Lean.PrettyPrinter.Formatter.checkWsBefore.formatter = do let st ← get if (st.leadWord != "") = true then Lean.PrettyPrinter.Formatter.pushLine else pure PUnit.unit
Equations
- Lean.PrettyPrinter.Formatter.checkNoWsBefore.formatter = modify fun st => { stxTrav := st.stxTrav, leadWord := "", isUngrouped := st.isUngrouped, mustBeGrouped := st.mustBeGrouped, stack := st.stack }
Equations
- Lean.PrettyPrinter.Formatter.pushNone.formatter = Lean.Syntax.MonadTraverser.goLeft
Equations
- Lean.PrettyPrinter.Formatter.interpolatedStr.formatter p = do let a ← Lean.Syntax.MonadTraverser.getCur Lean.PrettyPrinter.Formatter.visitArgs (Array.forM (fun chunk => match Lean.Syntax.isLit? Lean.interpolatedStrLitKind chunk with | some str => SeqRight.seqRight (Lean.PrettyPrinter.Formatter.push (Std.Format.text str)) fun x => Lean.Syntax.MonadTraverser.goLeft | none => p) (Array.reverse (Lean.Syntax.getArgs a)) 0 (Array.size (Array.reverse (Lean.Syntax.getArgs a))))
def
Lean.PrettyPrinter.Formatter.dbgTraceState.formatter
(label : String)
(p : Lean.PrettyPrinter.Formatter)
:
Equations
@[macroInline]
def
Lean.PrettyPrinter.Formatter.ite
{α : Type}
(c : Prop)
[h : Decidable c]
(t : Lean.PrettyPrinter.Formatter)
(e : Lean.PrettyPrinter.Formatter)
:
Equations
- Lean.PrettyPrinter.Formatter.ite c t e = if c then t else e
@[inline]
def
Lean.PrettyPrinter.Formatter.registerAlias
(aliasName : Lean.Name)
(v : Lean.PrettyPrinter.Formatter.FormatterAliasValue)
:
Equations
Equations
- Lean.PrettyPrinter.Formatter.instCoeFormatterFormatterAliasValue = { coe := Lean.Parser.AliasValue.const }
Equations
- Lean.PrettyPrinter.Formatter.instCoeForAllFormatterFormatterAliasValue = { coe := Lean.Parser.AliasValue.unary }
Equations
- Lean.PrettyPrinter.Formatter.instCoeForAllFormatterFormatterAliasValue_1 = { coe := Lean.Parser.AliasValue.binary }
Equations
- Lean.PrettyPrinter.format formatter stx = let cls := `PrettyPrinter.format.input; do let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.CoreM Lean.Format := fun y => do let options ← Lean.getOptions let table ← ST.Ref.get Lean.Parser.builtinTokenTable Lean.catchInternalId Lean.PrettyPrinter.backtrackExceptionId (do let discr ← StateRefT'.run (Lean.PrettyPrinter.Formatter.concat formatter { options := options, table := table }) { stxTrav := Lean.Syntax.Traverser.fromSyntax stx, leadWord := "", isUngrouped := false, mustBeGrouped := true, stack := #[] } let x : Unit × Lean.PrettyPrinter.Formatter.State := discr match x with | (x, st) => pure (Lean.Format.fill (Array.get! st.stack 0))) fun x => Lean.throwError (Lean.toMessageData "format: uncaught backtrack exception") if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "" ++ Lean.toMessageData (Lean.format stx) ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y