added rendering of zmagnitude and integer power

SKolodynski · Dec 26, 2024 · 9b68790 · 9b68790
1 parent c6cdaa4
commit 9b68790
Show file tree

Hide file tree

Showing 3 changed files with 16 additions and 3 deletions.
diff --git a/isar2html2.0/src/isar2html/Export2Html.fs b/isar2html2.0/src/isar2html/Export2Html.fs
@@ -1,7 +1,7 @@
 (*
     This file is part of isar2html2.0 - a tool for rendering IsarMathLib
 	theories in in HTML.
-    Copyright (C) 2022-2023  Slawomir Kolodynski
+    Copyright (C) 2022-2024  Slawomir Kolodynski
     This program is free software: you can redistribute it and/or modify
     it under the terms of the GNU General Public License as published by
     the Free Software Foundation, either version 3 of the License, or

diff --git a/isar2html2.0/src/isar2html/IsarSym2Latex.fs b/isar2html2.0/src/isar2html/IsarSym2Latex.fs
@@ -29,12 +29,24 @@ namespace iml
             if args[1].Length = 1 then args[1]+"^{"+args[0]+"}"
             else "("+args[1]+")"+"^{"+args[0]+"}"
 
+        /// expands integer power in the same way as the natural power, 
+        /// i.e. powz(n,x) --> x^n
+        
+        let macroPowz = macroPow 
+
+        /// macro that expands zmagnitude(z) --> |z|_N
+        let macroZmagnitude (args:string array) :string =
+            if args[0].Length = 1 then "| "+args[0]+"|\\<^isub>N "
+            else "\\left| "+args[0]+" \\right|\\<^isub>N "
+
 
         /// list of macros to be expanded, the first string is macro name, 
         /// the second is the template
         let macros : (string*((string array -> string))) array = 
             [| "Binom", macroBinom;
-                "pow",macroPow|]
+                "pow", macroPow;
+                "powz", macroPowz;
+                "zmagnitude", macroZmagnitude |]
 
         /// list of translations from Isar symbols to LaTeX symbols
         // TODO: read from a file maybe?
@@ -43,8 +55,10 @@ namespace iml
                  ("%","\\%")
                  ("$#","\\$\\!\\#\\!")
                  ("$+","\\ \\$\\!+\\ ")
+                 ("$*","\\ \\$\\!*\\ ")
                  ("$-","\\ \\$\\!-\\!")
                  ("$- ","\\ \\$\\!-\\ ")
+                 ("$\\leq ","\\ \\$\\!\\leq\\ ")
                  // ("$", "\\ \\$ ")
                  ("\\<longrightarrow>", "\\longrightarrow ")
                  (".", ".\\ ")

diff --git a/isar2html2.0/src/isar2html/isar2html.fsproj b/isar2html2.0/src/isar2html/isar2html.fsproj
@@ -9,7 +9,6 @@
     <Compile Include="IMLP_datatypes.fs" />
     <Compile Include="ProcessThys.fs" />
     <Compile Include="Export2Html.fs" />
-    <Compile Include="IMLP_datatypes.fs" />
     <Compile Include="IMLParser.fs" />
     <Compile Include="Program.fs" />
   </ItemGroup>