Packages

case class LeanRoutes()(implicit cc: castor.Context, log: Logger) extends Routes with Product with Serializable

Linear Supertypes
Serializable, Product, Equals, Routes, AnyRef, Any
Type Hierarchy
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. LeanRoutes
  2. Serializable
  3. Product
  4. Equals
  5. Routes
  6. AnyRef
  7. Any
Implicitly
  1. by any2stringadd
  2. by StringFormat
  3. by Ensuring
  4. by ArrowAssoc
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. Protected

Instance Constructors

  1. new LeanRoutes()(implicit cc: castor.Context, log: Logger)

Value Members

  1. def cancelParse(request: Request): String
    Annotations
    @post("/cancel", endpoints.this.post.<init>$default$2)
  2. def caskMetadata: RoutesEndpointsMetadata[LeanRoutes.this.type]
    Definition Classes
    Routes
  3. var channels: ArrayBuffer[WebSocketChannel]
  4. def codeGenDefs(): String
    Annotations
    @get("/codegen-defns", endpoints.this.get.<init>$default$2)
  5. def codeGenInducDefs(): String
    Annotations
    @get("/codegen-induc-defns", endpoints.this.get.<init>$default$2)
  6. def decorators: Seq[Decorator[_, _, _]]
    Definition Classes
    Routes
  7. def files(): String
    Annotations
    @get("/files", endpoints.this.get.<init>$default$2)
  8. def getMods(file: String): String
    Annotations
    @get("mods/:file", endpoints.this.get.<init>$default$2)
  9. def getModsJs(file: String): Value
  10. def inducDefn(request: Request): String
    Annotations
    @post("/inductive-definition", endpoints.this.post.<init>$default$2)
  11. def loadFile(name: String): Task[Unit]
  12. def loadFileReq(request: Request): String
    Annotations
    @post("/loadFile", endpoints.this.post.<init>$default$2)
  13. def log: Logger
  14. def memDefs(): String
    Annotations
    @get("/mem-defns", endpoints.this.get.<init>$default$2)
  15. def memInducDefs(): String
    Annotations
    @get("/mem-induc-defns", endpoints.this.get.<init>$default$2)
  16. def messenger: Logger
  17. def parse(request: Request): String
    Annotations
    @post("/lean-parse", endpoints.this.post.<init>$default$2)
  18. def parser: LeanParser
  19. def productElementNames: Iterator[String]
    Definition Classes
    Product
  20. def saveCode(): String
    Annotations
    @post("/save-code", endpoints.this.post.<init>$default$2)
  21. def send(s: String): Unit
  22. def sendErr(s: String): Unit
  23. def sendLog(s: String): Unit
  24. val sendLogger: Logger
  25. def showUserProfile(): WebsocketResult
    Annotations
    @websocket("/leanlib-websock", endpoints.this.websocket.<init>$default$2)