Pantograph.lean

@@ -95,11 +95,14 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
   goal_start (args: Protocol.GoalStart): MainM (CR Protocol.GoalStartResult) := do
     let state ← get
     let env ← Lean.MonadEnv.getEnv
-    let expr?: Except Protocol.InteractionError GoalState ← runTermElabM (match args.expr, args.copyFrom with
+    let expr?: Except _ GoalState ← runTermElabM (match args.expr, args.copyFrom with
-      | .some expr, .none => do
+      | .some expr, .none =>
-          match ← exprParse expr with
+        (match syntax_from_str env expr with
-          | .ok expr => return .ok (← GoalState.create expr)
+        | .error str => return .error <| errorI "parsing" str
-          | .error e => return .error e
+        | .ok syn => do
+          (match ← syntax_to_expr syn with
+          | .error str => return .error <| errorI "elab" str
+          | .ok expr => return .ok (← GoalState.create expr)))
       | .none, .some copyFrom =>
         (match env.find? <| copyFrom.toName with
         | .none => return .error <| errorIndex s!"Symbol not found: {copyFrom}"

Pantograph/Library.lean

@@ -76,12 +76,6 @@ def createCoreState (imports: Array String): IO Lean.Core.State := do
     (trustLevel := 1)
   return { env := env }
 
-/-- Execute a `CoreM` monad -/
-@[export pantograph_exec_core]
-def execCore {α} (context: Lean.Core.Context) (state: Lean.Core.State) (coreM: Lean.CoreM α):
-    IO (α × Lean.Core.State) :=
-  coreM.toIO context state
-
 @[export pantograph_env_catalog_m]
 def envCatalog: Lean.CoreM Protocol.EnvCatalogResult :=
   Environment.catalog ({}: Protocol.EnvCatalog)