Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Proposal: Add third source input type, "inline text" #20

Open
david-a-wheeler opened this issue May 22, 2023 · 1 comment
Open

Proposal: Add third source input type, "inline text" #20

david-a-wheeler opened this issue May 22, 2023 · 1 comment
Labels
Alg related to algorithms
Milestone

Comments

@david-a-wheeler
Copy link
Contributor

I propose adding a third source input type, "inline text". It just lets you put text into a text box, that would then be read. This text would also be included as part of the JSON or URL.

This would make it easy to create a proof that builds on an existing database and other proofs not in the database, by letting you temporarily add those proofs to what you're working on.

@expln
Copy link
Owner

expln commented May 24, 2023

I will implement this. Until then the below workarounds are available.

For local development - create a local text file and append it to the context via "plus" button. If you update content of the file then remove the source with the file via the "trash can" button (in the application header) and add it again. This is required because once content of a source is loaded it is never reloaded again.

For sharing via URL - save the file on GitHub (or any other location which then lets you download this file via HTTP GET without authentication). Add a URL of the file to your settings in the app. Provide an alias for that URL. Alias is not a required attribute but URLs without alias are not appearing in the source selector in the app header. Apply changes to settings and compose the proof you want to share using the file URL as one of the context sources. Then export your proof to URL and share with others. Others will be able to see your proof (if they don't have problems with loading your file). Your URL will not appear in the app settings for other people unless they check "don't ask for this URL" checkbox in the confirmation dialog. But even then your URL will not appear in the source selector for other people because your URL will not have an alias in their settings (aliases are not sharable). So overall this action will not introduce more and more sources in the app header for others. Here is an example of a GitHub URL I added to my settings to speed up loading of set.mm from the web - https://raw.githubusercontent.com/expln/metamath-lamp/master/src/metamath/test/resources/set-no-proofs._mm

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Alg related to algorithms
Projects
None yet
Development

No branches or pull requests

2 participants