FL: > I insist once again: why not adding a widget to open a file from the menu.
Actually, mmj2's GUI *does* have a GUI widget to open a menu. But the GUI is for loading & saving .mmp proof files, not the .mm database. Perhaps part of what is confusing about mmj2 is that it deals with *2* different kinds of files: * .mmp proof files. This is the proof format it natively saves & loads, e.g., File/Load and File/Save use *THIS* format. There currently isn't a command line option to load this; you can load one indirectly via a script using ProofAsstStartupProofWorksheet * .mm Metamath database files. It loads this database first, before you can interact with .mmp files. It has no way to edit/save this database file. Most programs don't have to deal with 2 different file formats, which is perhaps part of what makes this so confusing. Typically if there's a separate filetype, there'd be a command line option to set it or a "distinguished argument position" (usually the first one) to set it. E.g.: gawk [OPTIONS] -f program-file [ -- ] file ... gawk [ OPTIONS ] [ -- ] program-text file ... So perhaps the mmj2 CLI should be tweaked so that the .mmp files are the focus, at least when the GUI gets invoked. That has its advantages: if you want to edit a .mmp file, just double-click on it. In many ways that makes more sense, since only mmj2 can only edit .mmp files - not .mm files. With that in mind, maybe the mmj2 CLI should look more like this: mmj2 [OPTIONS] [.mmp FILE] -d METAMATH_DATABASE : Provides the path of the Metamath database. Long option name: --database -f SCRIPT_FILE : If present, run the script in file RUNTIME_SCRIPT and exit on completion. This is just its current RunParams mechanism. The script can run "RunProofAsstGUI" if it wants to enter GUI mode as part of the script. Long name: --script-file If "-f / --script-file" is not provided, mmj2 will: 1. load the METAMATH_DATABASE file as expressed with "-d". The filename is a pathname to the right database. If -d is not provided, it will use the last one it loaded, and failing that will search in "obvious directories" to make this easy. We can record "last one loaded" in a file somewhere in ~/.config or ~/.local. 2. If the .mmp FILE is stated & its path exists, it will load that. If it doesn't exist, it will fail fast (mmj2 takes a long time to start!). If no .mmp FILE is stated, a convenient default is loaded (that way the user can see SOMETHING and then load something else). I didn't see any obvious option flag names to steal from here: https://www.gnu.org/prep/standards/html_node/Option-Table.html Thoughts? --- David A. Wheeler -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/E1jZlDX-0003AO-2B%40rmmprod06.runbox.
