Added rule references

Colonial-Dev · Apr 23, 2024 · 141e272 · 141e272
1 parent c1964be
commit 141e272
Show file tree

Hide file tree

Showing 27 changed files with 1,171 additions and 20 deletions.
diff --git a/Cargo.lock b/Cargo.lock
diff --git a/Cargo.toml b/Cargo.toml
@@ -31,6 +31,7 @@ thiserror = "1.0.58"
 once_cell = "1.19.0"
 regex = "1.10.3"
 serde = { version = "1.0.197", features = ["derive"] }
+egui_extras = { version = "0.27.2", features = ["all_loaders"] }
 
 # Addl. WASM dependencies
 [target.'cfg(target_arch = "wasm32")'.dependencies]

diff --git a/src/main.rs b/src/main.rs
@@ -6,8 +6,8 @@ mod ui;
 fn main() {
     let native_options = eframe::NativeOptions {
         viewport: egui::ViewportBuilder::default()
-            .with_inner_size([720.0, 720.0])
-            .with_min_inner_size([720.0, 720.0]),
+            .with_inner_size([1024.0, 720.0])
+            .with_min_inner_size([1024.0, 720.0]),
             // TODO add icon
         ..Default::default()
     };

diff --git a/src/ui/mod.rs b/src/ui/mod.rs
@@ -46,6 +46,8 @@ pub struct Deduct {
 
 impl Deduct {
     pub fn new(cc: &eframe::CreationContext<'_>) -> Self {
+        egui_extras::install_image_loaders(&cc.egui_ctx);
+
         fonts_init(cc);
 
         if let Some(storage) = cc.storage {
@@ -68,8 +70,8 @@ impl Deduct {
         if let Some(ui) = self.new.try_create() {
             self.proof = Some(ui);
             self.vis.new_proof = false;
-            self.new.ready = false;
         }
+        self.new.ready = false;
     }
 
     fn handle_shortcuts(&mut self, ctx: &Context) {
@@ -180,32 +182,97 @@ impl eframe::App for Deduct {
             });
 
         });
-        
+
         egui::SidePanel::right("proof_rules")
             .resizable(false)
             .min_width(w * 0.25)
             .max_width(w * 0.25)
             .show(ctx, |ui| {
                 containers::ScrollArea::vertical().show(ui, |ui| {                   
+                    let tint = if self.prefs.dark_mode { Color32::WHITE } else { Color32::BLACK };
+
+                    macro_rules! rule {
+                        ($ui:ident, $path:literal) => {
+                            $ui.add(
+                                egui::Image::new(egui::include_image!($path))
+                                    .tint(tint)
+                                    .fit_to_fraction(
+                                        Vec2::new(0.975, f32::INFINITY)
+                                    )
+                            );
+                        };
+                    }
+
                     ui.collapsing("Operator Shorthands", |ui| {
-                        ui.label("Negation: ~");
-                        ui.label("Conjunction: ^ or &");
-                        ui.label("Disjunction: v");
-                        ui.label("Biconditional: <->");
-                        ui.label("Conditional: ->");
-                        ui.label("Contradiction: XX or #");
-                        ui.separator();
-                        ui.label("Necessity: []");
-                        ui.label("Possibility: <>");
+                        Grid::new("shorthand_grid")
+                        .striped(true)
+                        .num_columns(2)
+                        .show(ui, |ui| {
+                            let placeholder_tt = "Can be used to validate any arbitrary sentence.\nProofs that have reached the conclusion but still contain placeholders will be flagged as incomplete.";
+
+                            ui.label("Placeholder").on_hover_text(placeholder_tt);
+                            ui.label("?").on_hover_text(placeholder_tt);
+                            ui.end_row();
+
+                            ui.label("Negation");
+                            ui.label("~");
+                            ui.end_row();
+
+                            ui.label("Conjunction");
+                            ui.label("^ or &");
+                            ui.end_row();
+
+                            ui.label("Disjunction");
+                            ui.label("v");
+                            ui.end_row();
+
+                            ui.label("Conditional");
+                            ui.label("->");
+                            ui.end_row();
+
+                            ui.label("Biconditional");
+                            ui.label("<->");
+                            ui.end_row();
+
+                            ui.label("Contradiction");
+                            ui.label("XX or #");
+                            ui.end_row();
+
+                            ui.label("Necessity");
+                            ui.label("[ ]");
+                            ui.end_row();
+
+                            ui.label("Possibility");
+                            ui.label("<>");
+                            ui.end_row();
+                        });
                     });
 
                     ui.separator();
-                    ui.collapsing("Basic TFL", |ui| {});
-                    ui.collapsing("Derived TFL", |ui| {});
-                    ui.collapsing("System K", |ui| {});
-                    ui.collapsing("System T", |ui| {});
-                    ui.collapsing("System S4", |ui| {});
-                    ui.collapsing("System S5", |ui| {});
+
+                    ui.collapsing("Basic TFL", |ui| {
+                        rule!(ui, "static/rules/TFL.png");
+                    });
+
+                    ui.collapsing("Derived TFL", |ui| {
+                        rule!(ui, "static/rules/TFLD.png");
+                    });
+
+                    ui.collapsing("System K", |ui| {
+                        rule!(ui, "static/rules/K.png");
+                    });
+
+                    ui.collapsing("System T", |ui| {
+                        rule!(ui, "static/rules/RT.png");
+                    });
+
+                    ui.collapsing("System S4", |ui| {
+                        rule!(ui, "static/rules/R4.png");
+                    });
+
+                    ui.collapsing("System S5", |ui| {
+                        rule!(ui, "static/rules/R5.png");
+                    });
                 });
         });
 
@@ -349,7 +416,7 @@ fn fonts_init(cc: &eframe::CreationContext<'_>) {
 
     fonts.font_data.insert(
         "math".to_owned(),
-        FontData::from_static( include_bytes!("../static/latinmodern-math.otf") )
+        FontData::from_static( include_bytes!("static/latinmodern-math.otf") )
     );
 
     fonts.families.insert(

diff --git a/src/static/latinmodern-math.otf → src/ui/static/latinmodern-math.otf b/src/static/latinmodern-math.otf → src/ui/static/latinmodern-math.otf
diff --git a/src/ui/static/rules/.gitignore b/src/ui/static/rules/.gitignore
@@ -0,0 +1,3 @@
+*.aux
+*.out
+*.log
diff --git a/src/ui/static/rules/K.png b/src/ui/static/rules/K.png
diff --git a/src/ui/static/rules/Makefile b/src/ui/static/rules/Makefile
@@ -0,0 +1,18 @@
+.PRECIOUS: %.tex
+
+objects := $(patsubst texf/%.texf,%.svg,$(wildcard texf/*.texf))
+
+all: $(objects)
+	sed -i 's/rgb(0%, 0%, 0%)/rgb(100%, 100%, 100%)/g' *.svg
+
+%.tex: texf/%.texf texf/rule-template.tex forallxyyc.sty
+	pandoc -f latex -t latex --template texf/rule-template.tex -o $@ $<
+
+%.pdf: %.tex
+	pdflatex $*
+
+%.svg: %.pdf
+	pdf2svg $< $@
+
+clean:
+	rm -f *.tex *.pdf *.aux *.out *.log
diff --git a/src/ui/static/rules/R4.png b/src/ui/static/rules/R4.png
diff --git a/src/ui/static/rules/R5.png b/src/ui/static/rules/R5.png
diff --git a/src/ui/static/rules/RT.png b/src/ui/static/rules/RT.png
diff --git a/src/ui/static/rules/TFL.png b/src/ui/static/rules/TFL.png
diff --git a/src/ui/static/rules/TFLD.png b/src/ui/static/rules/TFLD.png
-Original file line number
+Diff line change
@@ -0,0 +1,3 @@
+    *.aux
+    *.out
+    *.log