Skip to content

Commit c646bbc

Browse files
epattersepatters
authored
Merge pull request #263 from ToposInstitute/diagram-pane
Toolbar and header for diagram editor
2 parents c03b2cf + 86dbc9d commit c646bbc

File tree

12 files changed

+218
-92
lines changed

12 files changed

+218
-92
lines changed

‎packages/frontend/src/diagram/diagram_editor.css‎

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
.diagram-head {
2+
display: flex;
3+
flex-direction: row;
4+
align-items: center;
5+
justify-content: space-between;
6+
7+
& .title {
8+
font-size: var(--h1-font-size);
9+
}
10+
11+
& .instance-of {
12+
font-size: var(--h4-font-size);
13+
}
14+
}

‎packages/frontend/src/diagram/diagram_editor.tsx‎

Lines changed: 54 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,10 @@
11
import { MultiProvider } from "@solid-primitives/context";
2-
import { useParams } from "@solidjs/router";
2+
import { A, useParams } from "@solidjs/router";
33
import { Match, Show, Switch, createResource, useContext } from "solid-js";
44
import invariant from "tiny-invariant";
55

66
import { RepoContext, RpcContext, getLiveDoc } from "../api";
7+
import { InlineInput } from "../components";
78
import { LiveModelContext, type ModelDocument, enlivenModelDocument } from "../model";
89
import {
910
type CellConstructor,
@@ -12,8 +13,10 @@ import {
1213
cellShortcutModifier,
1314
newFormalCell,
1415
} from "../notebook";
16+
import { BrandedToolbar, HelpButton } from "../page";
1517
import { TheoryLibraryContext } from "../stdlib";
1618
import type { InstanceTypeMeta } from "../theory";
19+
import { MaybePermissionsButton } from "../user";
1720
import { LiveDiagramContext } from "./context";
1821
import { type DiagramDocument, type LiveDiagramDocument, enlivenDiagramDocument } from "./document";
1922
import { DiagramMorphismCellEditor } from "./morphism_cell_editor";
@@ -26,6 +29,8 @@ import {
2629
newDiagramObjectDecl,
2730
} from "./types";
2831

32+
import "./diagram_editor.css";
33+
2934
export default function DiagramPage() {
3035
const params = useParams();
3136
const refId = params.ref;
@@ -47,20 +52,59 @@ export default function DiagramPage() {
4752
return enlivenDiagramDocument(refId, liveDoc, liveModel);
4853
});
4954

55+
return <DiagramDocumentEditor liveDiagram={liveDiagram()} />;
56+
}
57+
58+
export function DiagramDocumentEditor(props: {
59+
liveDiagram?: LiveDiagramDocument;
60+
}) {
5061
return (
51-
<Show when={liveDiagram()}>
52-
{(liveDiagram) => (
53-
<div class="growable-container">
54-
<div class="notebook-container">
55-
<DiagramNotebookEditor liveDiagram={liveDiagram()} />
62+
<div class="growable-container">
63+
<BrandedToolbar>
64+
<HelpButton />
65+
<MaybePermissionsButton permissions={props.liveDiagram?.liveDoc.permissions} />
66+
</BrandedToolbar>
67+
<Show when={props.liveDiagram}>
68+
{(liveDiagram) => <DiagramPane liveDiagram={liveDiagram()} />}
69+
</Show>
70+
</div>
71+
);
72+
}
73+
74+
/** Pane containing a diagram notebook plus a header for the title and model. */
75+
export function DiagramPane(props: {
76+
liveDiagram: LiveDiagramDocument;
77+
}) {
78+
const liveDoc = () => props.liveDiagram.liveDoc;
79+
const liveModel = () => props.liveDiagram.liveModel;
80+
81+
return (
82+
<div class="notebook-container">
83+
<div class="diagram-head">
84+
<div class="title">
85+
<InlineInput
86+
text={liveDoc().doc.name}
87+
setText={(text) => {
88+
liveDoc().changeDoc((doc) => {
89+
doc.name = text;
90+
});
91+
}}
92+
placeholder="Untitled"
93+
/>
94+
</div>
95+
<div class="instance-of">
96+
<div class="name">{liveModel().theory()?.instanceOfName}</div>
97+
<div class="model">
98+
<A href={`/model/${liveModel().refId}`}>{liveModel().liveDoc.doc.name}</A>
5699
</div>
57100
</div>
58-
)}
59-
</Show>
101+
</div>
102+
<DiagramNotebookEditor liveDiagram={props.liveDiagram} />
103+
</div>
60104
);
61105
}
62106

63-
/** Editor for a notebook defining a diagram in a model.
107+
/** Notebook editor for a diagram in a model.
64108
*/
65109
export function DiagramNotebookEditor(props: {
66110
liveDiagram: LiveDiagramDocument;
@@ -93,7 +137,7 @@ export function DiagramNotebookEditor(props: {
93137

94138
/** Editor for a notebook cell in a diagram notebook.
95139
*/
96-
export function DiagramCellEditor(props: FormalCellEditorProps<DiagramJudgment>) {
140+
function DiagramCellEditor(props: FormalCellEditorProps<DiagramJudgment>) {
97141
return (
98142
<Switch>
99143
<Match when={props.content.tag === "object"}>

‎packages/frontend/src/index.css‎

Lines changed: 21 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,11 +3,13 @@
33
--mono-font: Roboto Mono, monospace;
44

55
--main-color: black;
6+
--link-color: dimgray;
67
--topos-color: #53b6b2;
78

89
--h1-font-size: 3em;
910
--h2-font-size: 2em;
1011
--h3-font-size: 1.5em;
12+
--h4-font-size: 1.3em;
1113

1214
color: var(--main-color);
1315
font-family: var(--main-font);
@@ -31,8 +33,22 @@ body,
3133
}
3234

3335
a {
34-
color: #007481;
35-
text-decoration: none;
36+
color: var(--link-color);
37+
text-decoration: underline;
38+
}
39+
40+
.link-button {
41+
border: none;
42+
background-color: transparent;
43+
color: var(--link-color);
44+
font: inherit;
45+
text-decoration: underline;
46+
cursor: pointer;
47+
48+
&:disabled {
49+
text-decoration: none;
50+
cursor: auto;
51+
}
3652
}
3753

3854
h1,
@@ -53,6 +69,9 @@ h2 {
5369
h3 {
5470
font-size: var(--h3-font-size);
5571
}
72+
h4 {
73+
font-size: var(--h4-font-size);
74+
}
5675

5776
.popup {
5877
background: white;

‎packages/frontend/src/model/model_editor.css‎

Lines changed: 10 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,15 @@
1-
.model-title {
2-
font-size: var(--h1-font-size);
3-
}
4-
51
.model-head {
62
display: flex;
3+
flex-direction: row;
74
align-items: center;
85
justify-content: space-between;
6+
7+
& .title {
8+
font-size: var(--h1-font-size);
9+
}
10+
11+
& .theory-selector-button {
12+
font-size: var(--h4-font-size);
13+
max-width: 25%;
14+
}
915
}

‎packages/frontend/src/model/model_editor.tsx‎

Lines changed: 56 additions & 39 deletions
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,7 @@ import {
1717
import { BrandedToolbar, HelpButton } from "../page";
1818
import { TheoryLibraryContext } from "../stdlib";
1919
import type { ModelTypeMeta } from "../theory";
20-
import { PermissionsButton } from "../user";
20+
import { MaybePermissionsButton } from "../user";
2121
import { LiveModelContext } from "./context";
2222
import { type LiveModelDocument, type ModelDocument, enlivenModelDocument } from "./document";
2323
import { MorphismCellEditor } from "./morphism_cell_editor";
@@ -51,23 +51,19 @@ export default function ModelPage() {
5151
return enlivenModelDocument(refId, liveDoc, theories);
5252
});
5353

54-
return (
55-
<Show when={liveModel()}>
56-
{(liveModel) => <ModelDocumentEditor liveModel={liveModel()} />}
57-
</Show>
58-
);
54+
return <ModelDocumentEditor liveModel={liveModel()} />;
5955
}
6056

6157
export function ModelDocumentEditor(props: {
62-
liveModel: LiveModelDocument;
58+
liveModel?: LiveModelDocument;
6359
}) {
6460
const rpc = useContext(RpcContext);
6561
invariant(rpc, "Missing context for model document editor");
6662

6763
const navigate = useNavigate();
6864

69-
const createDiagram = async () => {
70-
const init = newDiagramDocument(props.liveModel.refId);
65+
const createDiagram = async (modelRefId: string) => {
66+
const init = newDiagramDocument(modelRefId);
7167

7268
const result = await rpc.new_ref.mutate({
7369
content: init as JsonValue,
@@ -81,8 +77,8 @@ export function ModelDocumentEditor(props: {
8177
navigate(`/diagram/${newRef}`);
8278
};
8379

84-
const createAnalysis = async () => {
85-
const init = newAnalysisDocument(props.liveModel.refId);
80+
const createAnalysis = async (modelRefId: string) => {
81+
const init = newAnalysisDocument(modelRefId);
8682

8783
const result = await rpc.new_ref.mutate({
8884
content: init as JsonValue,
@@ -100,38 +96,47 @@ export function ModelDocumentEditor(props: {
10096
<div class="growable-container">
10197
<BrandedToolbar>
10298
<HelpButton />
103-
<PermissionsButton permissions={props.liveModel.liveDoc.permissions} />
104-
<Show when={props.liveModel.theory()?.instanceTypes.length}>
105-
<IconButton onClick={createDiagram} tooltip="Create a diagram in this model">
99+
<MaybePermissionsButton permissions={props.liveModel?.liveDoc.permissions} />
100+
<Show when={props.liveModel?.theory()?.supportsInstances}>
101+
<IconButton
102+
onClick={() => props.liveModel && createDiagram(props.liveModel.refId)}
103+
tooltip="Create a diagram in this model"
104+
>
106105
<Network />
107106
</IconButton>
108107
</Show>
109-
<IconButton onClick={createAnalysis} tooltip="Analyze this model">
108+
<IconButton
109+
onClick={() => props.liveModel && createAnalysis(props.liveModel.refId)}
110+
tooltip="Analyze this model"
111+
>
110112
<ChartSpline />
111113
</IconButton>
112114
</BrandedToolbar>
113-
<ModelPane liveModel={props.liveModel} />
115+
<Show when={props.liveModel}>
116+
{(liveModel) => <ModelPane liveModel={liveModel()} />}
117+
</Show>
114118
</div>
115119
);
116120
}
117121

122+
/** Pane containing a model notebook plus a header with the title and theory.
123+
*/
118124
export function ModelPane(props: {
119125
liveModel: LiveModelDocument;
120126
}) {
121127
const theories = useContext(TheoryLibraryContext);
122128
invariant(theories, "Library of theories should be provided as context");
123129

124-
const liveModel = () => props.liveModel;
125-
const doc = () => props.liveModel.liveDoc.doc;
126-
const changeDoc = (f: (doc: ModelDocument) => void) => props.liveModel.liveDoc.changeDoc(f);
130+
const liveDoc = () => props.liveModel.liveDoc;
131+
127132
return (
128133
<div class="notebook-container">
129134
<div class="model-head">
130-
<div class="model-title">
135+
<div class="title">
131136
<InlineInput
132-
text={doc().name}
137+
text={liveDoc().doc.name}
133138
setText={(text) => {
134-
changeDoc((doc) => {
139+
liveDoc().changeDoc((doc) => {
135140
doc.name = text;
136141
});
137142
}}
@@ -141,34 +146,46 @@ export function ModelPane(props: {
141146
<TheorySelectorDialog
142147
theory={props.liveModel.theory()}
143148
setTheory={(id) => {
144-
changeDoc((model) => {
149+
liveDoc().changeDoc((model) => {
145150
model.theory = id;
146151
});
147152
}}
148153
theories={theories}
149-
disabled={doc().notebook.cells.some((cell) => cell.tag === "formal")}
154+
disabled={liveDoc().doc.notebook.cells.some((cell) => cell.tag === "formal")}
150155
/>
151156
</div>
152-
<LiveModelContext.Provider value={props.liveModel}>
153-
<NotebookEditor
154-
handle={liveModel().liveDoc.docHandle}
155-
path={["notebook"]}
156-
notebook={doc().notebook}
157-
changeNotebook={(f) => {
158-
changeDoc((doc) => f(doc.notebook));
159-
}}
160-
formalCellEditor={ModelCellEditor}
161-
cellConstructors={modelCellConstructors(liveModel().theory()?.modelTypes ?? [])}
162-
cellLabel={judgmentLabel}
163-
/>
164-
</LiveModelContext.Provider>
157+
<ModelNotebookEditor liveModel={props.liveModel} />
165158
</div>
166159
);
167160
}
168161

169-
/** Editor for a cell in a model of a double theory.
162+
/** Notebook editor for a model of a double theory.
163+
*/
164+
export function ModelNotebookEditor(props: {
165+
liveModel: LiveModelDocument;
166+
}) {
167+
const liveDoc = () => props.liveModel.liveDoc;
168+
169+
return (
170+
<LiveModelContext.Provider value={props.liveModel}>
171+
<NotebookEditor
172+
handle={liveDoc().docHandle}
173+
path={["notebook"]}
174+
notebook={liveDoc().doc.notebook}
175+
changeNotebook={(f) => {
176+
liveDoc().changeDoc((doc) => f(doc.notebook));
177+
}}
178+
formalCellEditor={ModelCellEditor}
179+
cellConstructors={modelCellConstructors(props.liveModel.theory()?.modelTypes ?? [])}
180+
cellLabel={judgmentLabel}
181+
/>
182+
</LiveModelContext.Provider>
183+
);
184+
}
185+
186+
/** Editor for a notebook cell in a model notebook.
170187
*/
171-
export function ModelCellEditor(props: FormalCellEditorProps<ModelJudgment>) {
188+
function ModelCellEditor(props: FormalCellEditorProps<ModelJudgment>) {
172189
return (
173190
<Switch>
174191
<Match when={props.content.tag === "object"}>

‎packages/frontend/src/model/theory_selector.css‎

Lines changed: 1 addition & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -1,22 +1,3 @@
1-
.theory-selector-button {
2-
border: none;
3-
font-size: 1.25em;
4-
padding: 16px;
5-
background-color: transparent;
6-
font-family: var(--main-font);
7-
cursor: pointer;
8-
font-weight: 500;
9-
10-
& .placeholder {
11-
color: darkgray;
12-
}
13-
14-
&:hover,
15-
& .placeholder:hover {
16-
color: var(--topos-color);
17-
}
18-
}
19-
201
.theory-selector {
212
display: flex;
223
flex-direction: column;
@@ -45,7 +26,7 @@
4526
}
4627

4728
& .group-name {
48-
font-weight: 600;
29+
font-weight: 500;
4930
padding-bottom: 1px;
5031
opacity: 35%;
5132
}

0 commit comments

Comments
 (0)