lots of stuff

client/src/components/hints.tsx

@@ -3,7 +3,11 @@ import * as React from 'react';
 import Markdown from './markdown';
 
 export function Hint({hint} : {hint: GameHint}) {
-  return <div className="message info"><Markdown>{hint.text}</Markdown></div>
+  return <div className="message information"><Markdown>{hint.text}</Markdown></div>
+}
+
+export function AdditionalHint({hint} : {hint: GameHint}) {
+  return <div className="message warning"><Markdown>{hint.text}</Markdown></div>
 }
 
 export function Hints({hints, showHidden} : {hints: GameHint[], showHidden: boolean}) {
@@ -13,6 +17,6 @@ export function Hints({hints, showHidden} : {hints: GameHint[], showHidden: bool
 
   return <>
     {openHints.map(hint => <Hint hint={hint} />)}
-    {showHidden && hiddenHints.map(hint => <Hint hint={hint} />)}
+    {showHidden && hiddenHints.map(hint => <AdditionalHint hint={hint}/>)}
   </>
 }

client/src/components/infoview/command_line.tsx

@@ -14,9 +14,9 @@ import * as leanMarkdownSyntax from 'lean4web/client/src/syntaxes/lean-markdown.
 import * as codeblockSyntax from 'lean4web/client/src/syntaxes/codeblock.json'
 import languageConfig from 'lean4/language-configuration.json';
 import { InteractiveDiagnostic, getInteractiveDiagnostics } from '@leanprover/infoview-api';
+import { Diagnostic } from 'vscode-languageserver-types';
 import { DocumentPosition } from '../../../../node_modules/lean4-infoview/src/infoview/util';
 import { useRpcSessionAtPos } from '../../../../node_modules/lean4-infoview/src/infoview/rpcSessions';
-
 import { InputModeContext, MonacoEditorContext, ProofContext, ProofStep } from './context'
 import { goalsToString } from './goals'
 import { InteractiveGoals } from './rpc_api'
@@ -106,9 +106,13 @@ export function CommandLine() {
       Promise.all(msgCalls).then((diagnostics : [InteractiveDiagnostic[]]) => {
         let tmpProof : ProofStep[] = []
 
+        let goalCount = 0
+
         steps.map((goals, i) => {
           // The first step has an empty command and therefore also no error messages
-          let messages = i ? diagnostics[i-1] : []
+          // Usually there is a newline at the end of the editors content, so we need to
+          // display diagnostics from potentally two lines in the last step.
+          let messages = i ? (i == steps.length - 1 ? diagnostics.slice(i-1).flat() : diagnostics[i-1]) : []
 
           // Filter out the 'unsolved goals' message
           messages = messages.filter((msg) => {
@@ -117,6 +121,26 @@ export function CommandLine() {
               msg.message.append[0].text === "unsolved goals")
           })
 
+          // If the number of goals reduce, show a message
+          if (goals.goals.length && goalCount > goals.goals.length) {
+            messages.unshift({
+              range: {
+                start: {
+                  line: i-1,
+                  character: 0,
+                },
+                end: {
+                  line: i-1,
+                  character: 0,
+                }},
+              severity: DiagnosticSeverity.Information,
+              message: {
+              text: 'intermediate goal solved 🎉'
+              }
+            })
+          }
+          goalCount = goals.goals.length
+
           // TODO: Check what happens if the code gets into a bad state and no goals are available
           if (!goals) {
             tmpProof.push({
@@ -177,20 +201,18 @@ export function CommandLine() {
     if (oneLineEditor && oneLineEditor.getValue() !== commandLineInput) {
       oneLineEditor.setValue(commandLineInput)
     }
-
-    // TODO: Is this the right place to load the goals once initially?
-    loadAllGoals()
   }, [commandLineInput])
 
   // React when answer from the server comes back
   useServerNotificationEffect('textDocument/publishDiagnostics', (params: PublishDiagnosticsParams) => {
     if (params.uri == editor.getModel().uri.toString()) {
       setProcessing(false)
-      if (!hasErrorsOrWarnings(params.diagnostics)) {
+      if (!hasErrors(params.diagnostics)) {
         setCommandLineInput("")
         editor.setPosition(editor.getModel().getFullModelRange().getEndPosition())
       }
     }
+    loadAllGoals() // TODO: instead of loading all goals every time, we could only load the last one
   }, []);
 
   useEffect(() => {
@@ -253,7 +275,6 @@ export function CommandLine() {
     const l = oneLineEditor.onKeyUp((ev) => {
       if (ev.code === "Enter") {
         runCommand()
-        loadAllGoals() // TODO: instead of loading all goals every time, we could only load the last one
       }
     })
     return () => { l.dispose() }
@@ -263,7 +284,6 @@ export function CommandLine() {
   const handleSubmit : React.FormEventHandler<HTMLFormElement> = (ev) => {
     ev.preventDefault()
     runCommand()
-    loadAllGoals() // TODO: instead of loading all goals every time, we could only load the last one
   }
 
   return <div className="command-line">
@@ -280,10 +300,17 @@ export function CommandLine() {
 
 /** Checks whether the diagnostics contain any errors or warnings to check whether the level has
    been completed.*/
-function hasErrorsOrWarnings(diags) {
+export function hasErrors(diags: Diagnostic[]) {
   return diags.some(
     (d) =>
       !d.message.startsWith("unsolved goals") &&
-      (d.severity == DiagnosticSeverity.Error || d.severity == DiagnosticSeverity.Warning)
+      (d.severity == DiagnosticSeverity.Error ) // || d.severity == DiagnosticSeverity.Warning
+  )
+}
+
+// TODO: Didn't manage to unify this with the one above
+export function hasInteractiveErrors (diags: InteractiveDiagnostic[]) {
+  return diags.some(
+    (d) => (d.severity == DiagnosticSeverity.Error ) // || d.severity == DiagnosticSeverity.Warning
   )
 }

client/src/components/infoview/context.ts

@@ -20,7 +20,7 @@ export type ProofStep = {
   /** Story relevant messages */
   hints: any        // TODO: Add correct type
   /** Errors and warnings */
-  errors: any       // TODO: Add correct type
+  errors: InteractiveDiagnostic[]       // TODO: Add correct type
 }
 
 /** The context storing the proof step-by-step for the command line mode */
@@ -37,12 +37,6 @@ export const ProofContext = React.createContext<{
   setProof: () => {} // TODO: implement me
 })
 
-
-
-
-
-
-
 // TODO: Is this still used?
 export const HintContext = React.createContext<{
   showHiddenHints : boolean,

client/src/components/infoview/goals.tsx

@@ -183,8 +183,6 @@ export const Goal = React.memo((props: GoalProps) => {
 export const MainAssumptions = React.memo((props: GoalProps2) => {
   const { goals, filter } = props
 
-
-
   const goal = goals[0]
   const filteredList = getFilteredHypotheses(goal.hyps, filter);
   const hyps = filter.reverse ? filteredList.slice().reverse() : filteredList;

client/src/components/infoview/info.tsx

@@ -128,7 +128,6 @@ const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => {
           <div className="goals-section">
             { goals &&  goals.goals.length > 0 && <>
               <MainAssumptions filter={goalFilter} key='mainGoal' goals={goals.goals} />
-              <ProofDisplay proof={proof}/>
               <OtherGoals filter={goalFilter} goals={goals.goals} />
             </>}
           </div>

client/src/components/infoview/infoview.css

@@ -4,8 +4,9 @@
   padding: 5px 10px;
   border-radius: 3px 3px 3px 3px;
 }
-.message.info {
+.message.information, .message.info {
   /* color: #059; */
+  color: #000;
   background-color: #DDF6FF;
 }
 .message.warning {
@@ -139,3 +140,20 @@
 .commandline-interface .content .tmp-pusher {
   flex: 1;
 }
+
+.undo-button {
+  border: 1px solid #bbb;
+  display: block;
+  padding-left: .3rem;
+  padding-right: .5rem;
+  float: right;
+  border-radius: .5rem;
+  background-color: #fff;
+  color: #888;
+}
+
+.undo-button:hover {
+  border: 1px solid #888;
+  background-color: #ffdcc7;
+  cursor: pointer;
+}

client/src/components/infoview/main.tsx

@@ -14,6 +14,10 @@ import { EditorContext, ConfigContext, ProgressContext, VersionContext } from '.
 import { WithRpcSessions } from '../../../../node_modules/lean4-infoview/src/infoview/rpcSessions';
 import { ServerVersion } from '../../../../node_modules/lean4-infoview/src/infoview/serverVersion';
 
+import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
+import { faDeleteLeft, faHome, faArrowRight, faArrowLeft, faRotateLeft } from '@fortawesome/free-solid-svg-icons'
+import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js'
+
 import { GameIdContext } from '../../app';
 import { useAppDispatch, useAppSelector } from '../../hooks';
 import { LevelInfo } from '../../state/api';
@@ -23,9 +27,10 @@ import Markdown from '../markdown';
 import { Infos } from './infos';
 import { AllMessages, Errors, WithLspDiagnosticsContext } from './messages';
 import { Goal } from './goals';
-import { InputModeContext, ProofContext, ProofStateContext, ProofStep } from './context';
+import { InputModeContext, MonacoEditorContext, ProofContext, ProofStateContext, ProofStep } from './context';
-import { CommandLine } from './command_line';
+import { CommandLine, hasErrors, hasInteractiveErrors } from './command_line';
 import { InteractiveDiagnostic } from '@leanprover/infoview/*';
+import { Button } from '../button';
 
 /** Wrapper for the two editors. It is important that the `div` with `codeViewRef` is
  * always present, or the monaco editor cannot start.
@@ -184,11 +189,14 @@ const goalFilter = {
 }
 
 /** The display of a single entered lean command */
-function Command({command} : {command: string}) {
+function Command({command, deleteProof} : {command: string, deleteProof: any}) {
   // The first step will always have an empty command
   if (!command) {return <></>}
   return <div className="command">
     {command}
+    <div className="undo-button" title="Delete this and future commands" onClick={deleteProof}>
+      <FontAwesomeIcon icon={faDeleteLeft} />
+    </div>
   </div>
 }
 
@@ -247,6 +255,8 @@ function Command({command} : {command: string}) {
 function GoalsTab({proofStep} : {proofStep: ProofStep}) {
   const [selectedGoal, setSelectedGoal] = React.useState<number>(0)
 
+  if (!proofStep.goals.length) {return <></>}
+
   return <div>
     <div className="tab-bar">
       {proofStep.goals.map((goal, i) => (
@@ -265,6 +275,8 @@ function GoalsTab({proofStep} : {proofStep: ProofStep}) {
 export function CommandLineInterface(props: {world: string, level: number, data: LevelInfo}) {
 
   const ec = React.useContext(EditorContext)
+  const editor = React.useContext(MonacoEditorContext)
+
   const gameId = React.useContext(GameIdContext)
   const {proof} = React.useContext(ProofContext)
 
@@ -283,33 +295,47 @@ export function CommandLineInterface(props: {world: string, level: number, data:
       []
   );
 
+  /** Delete all proof lines starting from a given line.
+   * Note that the first line (i.e. deleting everything) is `1`!
+   */
+  function deleteProof(line: number) {
+    return (ev) => {
+      editor.executeEdits("command-line", [{
+        range: monaco.Selection.fromPositions(
+          {lineNumber: line, column: 1},
+          editor.getModel().getFullModelRange().getEndPosition()
+        ),
+        text: '',
+        forceMoveMarkers: false
+      }])
+    }
+  }
+
   const completed = useAppSelector(selectCompleted(gameId, props.world, props.level))
 
-  /* Set up updates to the global infoview state on editor events. */
+  /* Set up updates to the global infoview seither you solved the level with warnings or your last command contains a syntax error Lean can't parseate on editor events. */
   const config = useEventResult(ec.events.changedInfoviewConfig) ?? defaultInfoviewConfig;
 
   const [allProgress, _1] = useServerNotificationState(
-      '$/lean/fileProgress',
+    '$/lean/fileProgress',
-      new Map<DocumentUri, LeanFileProgressProcessingInfo[]>(),
+    new Map<DocumentUri, LeanFileProgressProcessingInfo[]>(),
-      async (params: LeanFileProgressParams) => (allProgress) => {
+    async (params: LeanFileProgressParams) => (allProgress) => {
-          const newProgress = new Map(allProgress);
+      const newProgress = new Map(allProgress);
-          return newProgress.set(params.textDocument.uri, params.processing);
+      return newProgress.set(params.textDocument.uri, params.processing);
-      },
+    }, []
-      []
+  )
-  );
 
   const curUri = useEventResult(ec.events.changedCursorLocation, loc => loc?.uri);
 
   useClientNotificationEffect(
-      'textDocument/didClose',
+    'textDocument/didClose',
-      (params: DidCloseTextDocumentParams) => {
+    (params: DidCloseTextDocumentParams) => {
-          if (ec.events.changedCursorLocation.current &&
+      if (ec.events.changedCursorLocation.current &&
-              ec.events.changedCursorLocation.current.uri === params.textDocument.uri) {
+        ec.events.changedCursorLocation.current.uri === params.textDocument.uri) {
-              ec.events.changedCursorLocation.fire(undefined)
+        ec.events.changedCursorLocation.fire(undefined)
-          }
+      }
-      },
+    }, []
-      []
+  )
-  );
 
   const serverVersion =
       useEventResult(ec.events.serverRestarted, result => new ServerVersion(result.serverInfo?.version ?? ''))
@@ -331,7 +357,7 @@ export function CommandLineInterface(props: {world: string, level: number, data:
             {/* <Infos /> */}
             <div className="tmp-pusher"></div>
             {proof.map((step, i) => {
-              if (i == proof.length - 1 && step.errors.length) {
+              if (i == proof.length - 1 && hasInteractiveErrors(step.errors)) {
                 // if the last command contains an error, we should not display it
                 // as it will be overwritten by the next entered command
                 return <div>
@@ -339,11 +365,25 @@ export function CommandLineInterface(props: {world: string, level: number, data:
                 </div>
               }
               else {
-                return <div className="step">
+                return <>
-                  <Command command={step.command} />
+                  <div className="step">
-                  <Errors errors={step.errors} commandLineMode={true}/>
+                    <Command command={step.command} deleteProof={deleteProof(i)}/>
-                  <GoalsTab proofStep={step} />
+                    <Errors errors={step.errors} commandLineMode={true}/>
-                </div>
+                    <GoalsTab proofStep={step}/>
+                  </div>
+                  {/* Show a message that there are no goals left */}
+                  {!step.goals.length && (
+                    <div className="message information">
+                      {completed ?
+                        <p>Level completed! 🎉</p> :
+                        <p>
+                          <b>no goals left</b><br />
+                          <i>This probably means you solved the level with warnings</i>
+                        </p>
+                      }
+                    </div>
+                  )}
+                </>
               }
             })}
           </div>

client/src/components/landing_page.css

@@ -91,7 +91,7 @@ div.image {
 .info {
   margin-top: 5px;
   margin-bottom: 15px;
-  width: calc(100% - 20px);
+  /* width: calc(100% - 20px); */
   border-collapse: collapse;
 }
 

client/src/components/level.css

@@ -215,11 +215,17 @@ td code  {
 /* TODO: Create a nice style and move this to a better place */
 
 .exercise .command {
-  background-color: rgb(167, 167, 167);
+  /* background-color: rgb(167, 167, 167); */
+  border: 1px solid #bbb;
+  background-color: #eee;
+  padding: .5rem;
+  border-radius: .5rem;
+  margin-top: 1rem;
 }
 
 .exercise .step {
-  background-color: #ffeb91;
+  /* background-color: #e6f0f4; */
   margin-top: 5px;
   margin-bottom: 5px;
+  /* border: 3px dotted rgb(88, 131, 24); */
 }

client/src/components/level.tsx

@@ -198,7 +198,7 @@ function PlayableLevel({worldId, levelId}) {
         <div ref={chatPanelRef} className="chat-panel">
           <div className="chat">
             {level?.data?.introduction &&
-              <div className="message info">
+              <div className="message information">
                 <Markdown>{level?.data?.introduction}</Markdown>
               </div>
             }
@@ -207,11 +207,11 @@ function PlayableLevel({worldId, levelId}) {
             })}
             {completed &&
               <>
-                <div className="message info">
+                <div className="message information">
                   Level completed! 🎉
                 </div>
                 {level?.data?.conclusion?.trim() &&
-                  <div className="message info">
+                  <div className="message information">
                     <Markdown>{level?.data?.conclusion}</Markdown>
                   </div>
                 }
@@ -266,7 +266,7 @@ function Introduction({worldId}) {
     <LevelAppBar isLoading={gameInfo.isLoading} levelTitle="Einführung" worldId={worldId} levelId={0} />
     <div style={gameInfo.isLoading ? {display: "none"} : null} className="exercise-panel">
       <div className="introduction-panel">
-        <div className="message info">
+        <div className="message information">
             <Markdown>
               {gameInfo.data?.worlds.nodes[worldId].introduction}
             </Markdown>

server/GameServer/FileWorker.lean

@@ -75,12 +75,12 @@ partial def findForbiddenTactics (inputCtx : Parser.InputContext)
     if 0 < val.length ∧ val.data[0]!.isAlpha ∧ not (allowed.contains val) then
       let val := val.dropRightWhile (fun c => c == '!' || c == '?') -- treat `simp?` and `simp!` like `simp`
       match levelParams.tactics.find? (fun t => t.name.toString == val) with
-      | none => addErrorMessage info s!"You have not unlocked the tactic '{val}' yet!"
+      | none => addWarningMessage info s!"You have not unlocked the tactic '{val}' yet!"
       | some tac =>
         if tac.locked then
-          addErrorMessage info s!"You have not unlocked the tactic '{val}' yet!"
+          addWarningMessage info s!"You have not unlocked the tactic '{val}' yet!"
         else if tac.disabled then
-          addErrorMessage info s!"The tactic '{val}' is disabled in this level!"
+          addWarningMessage info s!"The tactic '{val}' is disabled in this level!"
   | .ident info rawVal val preresolved =>
       let ns ←
         try resolveGlobalConst (mkIdent val)
@@ -90,17 +90,17 @@ partial def findForbiddenTactics (inputCtx : Parser.InputContext)
           | return () -- not a theroem -> ignore
         let lemmasAndDefs := levelParams.lemmas ++ levelParams.definitions
         match lemmasAndDefs.find? (fun l => l.name == n) with
-        | none => addErrorMessage info s!"You have not unlocked the lemma/definition '{n}' yet!"
+        | none => addWarningMessage info s!"You have not unlocked the lemma/definition '{n}' yet!"
         | some lem =>
           if lem.locked then
-            addErrorMessage info s!"You have not unlocked the lemma/definition '{n}' yet!"
+            addWarningMessage info s!"You have not unlocked the lemma/definition '{n}' yet!"
           else if lem.disabled then
-            addErrorMessage info s!"The lemma/definition '{n}' is disabled in this level!"
+            addWarningMessage info s!"The lemma/definition '{n}' is disabled in this level!"
-where addErrorMessage (info : SourceInfo) (s : MessageData) :=
+where addWarningMessage (info : SourceInfo) (s : MessageData) :=
   modify fun st => { st with
     messages := st.messages.add {
       fileName := inputCtx.fileName
-      severity := MessageSeverity.error
+      severity := MessageSeverity.warning
       pos      := inputCtx.fileMap.toPosition (info.getPos?.getD 0)
       data     := s
     }