/[mojave]/metaprl/support/shell/shell_browser.ml
ViewVC logotype

Log of /metaprl/support/shell/shell_browser.ml

Parent Directory Parent Directory | Revision Log Revision Log


Links to HEAD: (view) (download) (annotate)
Sticky Revision:

Revision 9655 - (view) (download) (annotate) - [select for diffs]
Modified Tue Oct 31 18:16:04 2006 UTC (14 years, 7 months ago) by nogin
File length: 58188 byte(s)
Diff to previous 8585
- In browser mode, use "/foo" relative URLs instead of the
  "https://host:port/foo" ones whenever possible. This is needed in order to
  make it easier to access the MetaPRL session indirectly (e.g. via an ssh
  tunnel).

  Only three places will now use the FQ URL:
   - startup message 
   - autologin file
   - form passed to the external editor

- A few display form fixes and improvements.



Revision 8585 - (view) (download) (annotate) - [select for diffs]
Modified Tue Jan 24 04:51:23 2006 UTC (15 years, 5 months ago) by nogin
File length: 58486 byte(s)
Diff to previous 8581
- When no port is given (or when -port 0 is given), use the first free port
  starting with the default 60,000.

- If the HTTP server failed to start up (the port is in use, etc), print a
  better error message.


Revision 8581 - (view) (download) (annotate) - [select for diffs]
Modified Tue Jan 24 03:59:17 2006 UTC (15 years, 5 months ago) by nogin
File length: 57784 byte(s)
Diff to previous 8579
In the readonly installation mode, we currently do not have doc/htmlman - so
when doc/htmlman is unavailable, we need to point to http://metaprl.org/
instead.


Revision 8579 - (view) (download) (annotate) - [select for diffs]
Modified Tue Jan 24 02:42:12 2006 UTC (15 years, 5 months ago) by nogin
File length: 57584 byte(s)
Diff to previous 8029
Made the default browser command configurable via the mk/config.


Revision 8029 - (view) (download) (annotate) - [select for diffs]
Modified Fri Oct 28 15:06:43 2005 UTC (15 years, 7 months ago) by nogin
File length: 57564 byte(s)
Diff to previous 7722
More changes related to chaising unused variables

Revision 7722 - (view) (download) (annotate) - [select for diffs]
Modified Mon Sep 19 20:45:42 2005 UTC (15 years, 9 months ago) by nogin
File length: 57815 byte(s)
Diff to previous 7563
Changes related to CVS -> Subversion switch:

- Updated the documentation to use svn.metaprl.org URLs instead of the
  cvs.metaprl.org ones.

- Updated checkout instructions (both read-only and read-write) to talk about
  subversion instead of CVS.

- Updated *.eps and *.ai to be svn:eol-style=native,
  svn:mime-type=application/postscript.


Revision 7563 - (view) (download) (annotate) - [select for diffs]
Modified Thu Jul 7 02:30:10 2005 UTC (15 years, 11 months ago) by nogin
File length: 57815 byte(s)
Diff to previous 7402
This is a huge commit that is mostly no-op:

- Updated the standard preamble text to point to the correct location for the
  documentation and to avoid mentioning Nuprl.

- Changed "Nuprl-Light" -> "MetaPRL" in a few places (amazingly, we still had
  those).

- Split the Nuprl_font file into Mpfont and Mpsymbols.

- Protected a few display forms in ITT with a "doc docoff".


Revision 7402 - (view) (download) (annotate) - [select for diffs]
Modified Sat Jun 25 02:21:42 2005 UTC (16 years ago) by nogin
File length: 57827 byte(s)
Diff to previous 7360
Do a backup_all before processing a syscall. This should cure the most common
cases of bad "!rebuild; !restart" interactions.


Revision 7360 - (view) (download) (annotate) - [select for diffs]
Modified Mon Jun 6 02:14:06 2005 UTC (16 years ago) by nogin
File length: 57833 byte(s)
Diff to previous 7355
Opname "shortening" in display forms.

Changed the display forms API making the shortener an integral part of the
dform_base type. Now all the standard display uses the shortener properly. I
also changed the shortener type adding an op_kind (OpnameNormal/OpnameToken
flag) to the list of its arguments and change the slot[opname:t] display to
use the shortener.


Revision 7355 - (view) (download) (annotate) - [select for diffs]
Modified Sat Jun 4 19:27:45 2005 UTC (16 years ago) by nogin
File length: 57895 byte(s)
Diff to previous 7264
Made the dform_base type abstract.


Revision 7264 - (view) (download) (annotate) - [select for diffs]
Modified Thu May 12 07:57:30 2005 UTC (16 years, 1 month ago) by nogin
File length: 57897 byte(s)
Diff to previous 6444
ToploopIgnoreError/ToploopIgnoreExn should not cause the http server to die.


Revision 6444 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jan 19 21:15:05 2005 UTC (16 years, 5 months ago) by nogin
File length: 57654 byte(s)
Diff to previous 6347
No-op: removed a number of unused "open" statements


Revision 6347 - (view) (download) (annotate) - [select for diffs]
Modified Thu Dec 9 07:24:13 2004 UTC (16 years, 6 months ago) by nogin
File length: 57739 byte(s)
Diff to previous 6248
Browser interface fixes:
- Menu labels need to be HTML escaped.
- "slot" mechanism should use the "src" display forms form the local theory,
  not for the "top" bookmark.


Revision 6248 - (view) (download) (annotate) - [select for diffs]
Modified Fri Oct 22 23:07:58 2004 UTC (16 years, 8 months ago) by nogin
File length: 57754 byte(s)
Diff to previous 6052
A bit of standartization of debug variables:
- the "debug_foo" variable should have debug_name set to "foo", not "debug_foo"
  (less typing on the command line this way)
- debug_description should be the same for all the instances of the same variable
  and it should be sufficiently descriptive to be meaningful w/o knowing which
  file it came from (see http://metaprl.org/developer-guide/debugging.html)


Revision 6052 - (view) (download) (annotate) - [select for diffs]
Modified Sat Jul 10 05:36:10 2004 UTC (16 years, 11 months ago) by nogin
File length: 57754 byte(s)
Diff to previous 5992
Added a "-batch" command-line option to MetaPRL that causes MetaPRL to be
a bit quieter. "-batch" implies "-cli".


Revision 5992 - (view) (download) (annotate) - [select for diffs]
Modified Tue Jun 22 04:45:14 2004 UTC (17 years ago) by nogin
File length: 57752 byte(s)
Diff to previous 5981
Copying Jason's branch commit to the trunk.


Revision 5981 - (view) (download) (annotate) - [select for diffs]
Modified Mon Jun 21 13:21:46 2004 UTC (17 years ago) by jyh
File length: 57593 byte(s)
Diff to previous 5976
For some reason IE insists on caching the output page.
Allow URLs of the form /nocache/xxx/url, where xxx is a random number.


Revision 5976 - (view) (download) (annotate) - [select for diffs]
Modified Mon Jun 21 10:26:32 2004 UTC (17 years ago) by nogin
File length: 57443 byte(s)
Diff to previous 5970
When for some reason the content URL instructed us to chdir to one place and
we ended up in another, reload the content frame.


Revision 5970 - (view) (download) (annotate) - [select for diffs]
Modified Mon Jun 21 05:29:35 2004 UTC (17 years ago) by nogin
File length: 57468 byte(s)
Diff to previous 5965
- I've changed the browser interface to be the default one. Use the "-cli"
option to get the command-line interface (mpxterm and mpkonsole scripts
will set the -cli flag automatically).
- The SSL and THREADS will now be enabled by default (this only has effects
when you do _not_ already have an mk/config)


Revision 5965 - (view) (download) (annotate) - [select for diffs]
Modified Mon Jun 21 04:45:22 2004 UTC (17 years ago) by nogin
File length: 57504 byte(s)
Diff to previous 5962
1) It is now possible to specify the host name to use (in SSL certificates
and URLs) using either the -browser_hostname option, or MP_BROWSER_HOSTNAME
environment variable. By default, the Unix.gethostname is used.

2) The SSL certificates are now kept in ~/.metaprl/ssl/$MP_BROWSER_HOSTNAME
directory and will be created automatically by MetaPRL _on startup_ (not by
omake). This ensures that:
 - The SSL certificates will have the hostname matching the one used in URLs
 - The SSL certificates will _not_ be cleaned by "omake [real]clean", which
   means that the browser will not complain about a suddenly changed cert.
 - The SSL certs are not bound to a specific source tree (again, the browser
   will not complain when you switch from one tree to another).

3) If /usr/bin/htmlview or /usr/bin/mozilla exists, it will be used as a
default value for the browser command (-browser_command/MP_BROWSER_COMMAND
still take precedence, of course).

4) Updated the message printed by MetaPRL on start up to make it more clear
that:
 - The browser command was called (of course, it only says that when the
   browser command is specified) and the user only needs to intervene
   manually if the browser fails to start up automatically.
 - The file URL will not require a log in, but the https one will (Nathan
   requested this).


Revision 5962 - (view) (download) (annotate) - [select for diffs]
Modified Mon Jun 21 03:40:44 2004 UTC (17 years ago) by jyh
File length: 57201 byte(s)
Diff to previous 5960
Fixed some browser problems with IE.
Note: you can now use line numbers when editing files.
This update was performed using the browser interface.


Revision 5960 - (view) (download) (annotate) - [select for diffs]
Modified Mon Jun 21 00:26:43 2004 UTC (17 years ago) by jyh
File length: 57001 byte(s)
Diff to previous 5957
Made editing much more robust, so that you don't lost work
on a restart.


Revision 5957 - (view) (download) (annotate) - [select for diffs]
Modified Sun Jun 20 15:54:04 2004 UTC (17 years ago) by jyh
File length: 55277 byte(s)
Diff to previous 5955
Fixed Javascript string escapes.


Revision 5955 - (view) (download) (annotate) - [select for diffs]
Modified Sun Jun 20 03:46:59 2004 UTC (17 years ago) by jyh
File length: 55055 byte(s)
Diff to previous 5951
Fixed the problem with going to some random directory on restart.

Note:
   Mozilla tries to remember subframe locations on location.reload();
   To avoid this, use location.href = location.href.


Revision 5951 - (view) (download) (annotate) - [select for diffs]
Modified Sat Jun 19 22:39:37 2004 UTC (17 years ago) by jyh
File length: 54935 byte(s)
Diff to previous 5942
Output is persistent.


Revision 5942 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jun 18 21:38:45 2004 UTC (17 years ago) by jyh
File length: 55407 byte(s)
Diff to previous 5940
This is probably the final round of changes.
All windows are internal now.
Coming in in about 30min.


Revision 5940 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jun 18 18:09:37 2004 UTC (17 years ago) by jyh
File length: 54783 byte(s)
Diff to previous 5939
Add the session and directory to the title bar.


Revision 5939 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jun 18 18:02:14 2004 UTC (17 years ago) by jyh
File length: 54716 byte(s)
Diff to previous 5935
Re-use the HTTP socket on a restart.  The socket descriptor
and challenge are saved in the environment.  So this means
it won't work on Windows, where sockets do not have integer
descriptors.  Have to think about how to do that, or else
just disable the feature on Windows.


Revision 5935 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jun 18 06:32:00 2004 UTC (17 years ago) by nogin
File length: 53650 byte(s)
Diff to previous 5933
Adding the MetaPRL "shortcut" icon (both Mozilla and IE should be happy, hopefully).


Revision 5933 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jun 18 06:15:32 2004 UTC (17 years ago) by nogin
File length: 53650 byte(s)
Diff to previous 5932
Added MetaPRL version to the Welcome page. HTML could be nicer, though.


Revision 5932 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jun 18 05:44:31 2004 UTC (17 years ago) by nogin
File length: 53575 byte(s)
Diff to previous 5919
- The "/manual/filename" URIs now serve the documentation from the
  doc/htmlman directory in the local MetaPRL installation.
- Added a bit of content to the MetaPRL welcome page.
- The body page should not reset the hostname to the default value.


Revision 5919 - (view) (download) (annotate) - [select for diffs]
Modified Thu Jun 17 19:16:29 2004 UTC (17 years ago) by jyh
File length: 53234 byte(s)
Diff to previous 5913
Fixed the refresh problem.  The issue with refresh was that it was lazy:
don't do a remount unless the directory has changed.  Added a force_flag
to the chdir function.


Revision 5913 - (view) (download) (annotate) - [select for diffs]
Modified Thu Jun 17 05:21:25 2004 UTC (17 years ago) by nogin
File length: 52890 byte(s)
Diff to previous 5912
Centralized the shell handling of the "display method" data (including
display mode, display base, display width and display destination).

In partucilar:
- The set_dfmode function now takes effect immediatelly (no need to
cd "/";; cd "/back/where/we/were";;  after a set_dfmode).
- The bug with "prl" mode output in "-browser" sessions seems to be gone!
- The separation between display modes ("prl"/"src"/"html"/"tex"/"raw"/etc)
and display "types" (i.e. destinations - Tex/Text/Browser) is now more
complete (in fact we now _never_ convert modes into types).
- The code for handling the display method data is no longer duplicated 5 times
(now all code is in shell_core and proof_edit).


Revision 5912 - (view) (download) (annotate) - [select for diffs]
Modified Thu Jun 17 03:48:54 2004 UTC (17 years ago) by jyh
File length: 52798 byte(s)
Diff to previous 5908
Separate "shell" sessions from "browser" sessions.

Bah, browser identifiers are back to integers...  Sorry about the
change yet again, the proper URLs are /session/%d/...


Revision 5908 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jun 16 18:56:29 2004 UTC (17 years ago) by jyh
File length: 53168 byte(s)
Diff to previous 5907
This should fix the refresh problem.
Tracked down a bug in restart that was jumping to the previous location
(ouch, these are hard to find).


Revision 5907 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jun 16 07:53:11 2004 UTC (17 years ago) by jyh
File length: 52958 byte(s)
Diff to previous 5898
I thought I should commit before we get too out of date.
This is a partial commit; I'll finish off the loose ends
in the morning.

This adds the /fs path for viewing the Unix filesystem.

Notes on this commit:
   1. Removed the "view_*" functions in Shell_core.  These
      duplicated work, and were pretty pointless.

      However, in the browser, I see the following problem:
      the "refresh" function is not called correctly.  The symptom
      is that the display is in "prl" mode.  The solution, until
      I fix in the morning, is to call "refresh ()" explicitly.

   2. Use cd "/fs" to view the filesystem.  However, file editing
      with "cd" is not currently implemented; it is waiting on
      the recent discussion on "proposal for handling pwd()"
      on the onlynews@metaprl.org list.

   3. Shell identifiers now strings.  Sorry for this change, but
      it makes the implementation much easier.  The proper
      path is https://..../session/id1/frameset.


Revision 5898 - (view) (download) (annotate) - [select for diffs]
Modified Mon Jun 14 04:34:44 2004 UTC (17 years ago) by jyh
File length: 52542 byte(s)
Diff to previous 5897
Fixed the problem with !restart.
Added the commands to the File menu.


Revision 5897 - (view) (download) (annotate) - [select for diffs]
Modified Mon Jun 14 02:57:43 2004 UTC (17 years ago) by jyh
File length: 52623 byte(s)
Diff to previous 5892
This is the new file model.

Differences:
   1. Instead of "save ()", use "backup ()".
   2. Instead of "export ()", use "save ()".
   3. "backup_all ()" is called automatically when you exit.
   4. If you really want to quit without saving, use "abort ()".
   5. To revert to the last save, use "revert ()".

Just to be clear, *only* the files that you have modified
are backed-up when you quit.


Revision 5892 - (view) (download) (annotate) - [select for diffs]
Modified Sun Jun 13 00:39:56 2004 UTC (17 years ago) by jyh
File length: 52595 byte(s)
Diff to previous 5886
Fixed the ls problem I believe.
Save session state.  This also saves the current directory.
Every session has its own persistent history, etc.


Revision 5886 - (view) (download) (annotate) - [select for diffs]
Modified Sat Jun 12 01:23:11 2004 UTC (17 years ago) by nogin
File length: 52742 byte(s)
Diff to previous 5885
Moved the initialization of common paths ($MPLIB, $MP_HOME, ~/.metaprl, etc)
into the mllib/setup module.


Revision 5885 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jun 11 20:09:32 2004 UTC (17 years ago) by jyh
File length: 53406 byte(s)
Diff to previous 5883
Adding support for saving session state in files.


Revision 5883 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jun 11 16:33:41 2004 UTC (17 years ago) by jyh
File length: 53504 byte(s)
Diff to previous 5876
Synchronization fixes.


Revision 5876 - (view) (download) (annotate) - [select for diffs]
Modified Thu Jun 10 21:53:34 2004 UTC (17 years ago) by jyh
File length: 52880 byte(s)
Diff to previous 5870
Resolved the Not_found problem.  So hard to track down:(


Revision 5870 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jun 9 20:56:34 2004 UTC (17 years ago) by jyh
File length: 52371 byte(s)
Diff to previous 5869
Updated the browser to the new state model.

Note: we still get less parallelism than we would hope, because
refinement shares the (unique) output channel.  This could be fixed
by making stdout/stderr private variables.  Or we could just accept
that output will be jumbled if multiple threads are running.

I haven't actually enabled multiple threads yet in Http_simple.
That's next.


Revision 5869 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jun 9 18:38:02 2004 UTC (17 years ago) by jyh
File length: 50168 byte(s)
Diff to previous 5836
This modifies the infrastructure for threads.  Here is the model:

    1. Each thread has a current state, and each state has a set
       of global variables.

    2. State variables must be locked before being used.

    3. State variables come in two types: shared and private.
       Each state has its own copy of the private variables.

For example, each job in the shell has its own state, and its
own copy of the Shell.info struct.  States are managed implicitly,
so global variables look just like global variables.  Access is
managed with the State.read/State.write routines.

Here is an example of usage for a shared variable:

    let global_entry = State.shared_val "debug" (ref 0)

    let get () =
       State.read global_entry (fun x -> !x)

    let incr () =
       State.write global_entry (fun x -> x := !x + 1)

For private variable, you have to supply a "fork" function that
is used to copy the value.  Each thread/state will have its own copy
of the variable.  The other functions remain the same.

    let global_entry = State.shared_val "debug" (ref 0) (fun x -> ref !x)

All the State.* functions are wrappers that take a function argument.  The
value is locked on entry into the function, and unlocked when the function exits.
Exceptions are handled correctly.

Don't use Mutex if you can help it!!!  The Mutex functions do not
handle exceptions correctly.  Use the State module instead.

NOTES:

   1. I removed the Java interface...  It was just getting to be too much
      of a hassle.  We can ressurect it if we ever want it again.

   2. This is just the infrastructure pass.  The global values used by the
      browser need to be updated to the new model.


Revision 5836 - (view) (download) (annotate) - [select for diffs]
Modified Sun May 30 20:39:53 2004 UTC (17 years ago) by jyh
File length: 50655 byte(s)
Diff to previous 5834
Minor fixes.
Tested on win32 and mojave clients.


Revision 5834 - (view) (download) (annotate) - [select for diffs]
Modified Sun May 30 19:55:20 2004 UTC (17 years ago) by jyh
File length: 50569 byte(s)
Diff to previous 5833
Minor changes to get Win32 to run.
Note that Unix.fstat and Unix.fchmod do not work on
win32.


Revision 5833 - (view) (download) (annotate) - [select for diffs]
Modified Sun May 30 19:12:31 2004 UTC (17 years ago) by jyh
File length: 50501 byte(s)
Diff to previous 5829
Added some additional functions.  Status: tested with and without SSL on
RH9; not tested on mojave clients; mostly tested on win32.  I'll check
the others after this commit.  Tested against Mozilla and IE.  It should
be clean, but let me know if you see problems!

Added the following functions to the toploop:
   !ls: int                -- filesystem directory listing
   !cd: string -> int      -- change directory
   !pwd: string            -- print working directory
   !mkdir: string -> int   -- create a new directory
   !rm: string -> int      -- remove a file
   !edit: string -> int    -- edit a file
   !omake: int             -- rebuild the system
   !restart: int           -- restart MetaPRL
   !cvs: string -> int     -- CVS operations
Note that the syntax of these "syscall" commands uses dereferencing.

These functions work with the terminal and browser interfaces
(with slightly different behavior).


Revision 5829 - (view) (download) (annotate) - [select for diffs]
Modified Sat May 29 05:42:51 2004 UTC (17 years ago) by jyh
File length: 44640 byte(s)
Diff to previous 5826
New SSL method to provide a "standard" socket interface,
except certificates are required for some calls.

Tested on RedHat 9.
   - Not tested on old Redhat mojave clients.
   - Not tested on win32 (that is next).


Revision 5826 - (view) (download) (annotate) - [select for diffs]
Modified Fri May 28 16:11:44 2004 UTC (17 years ago) by jyh
File length: 44075 byte(s)
Diff to previous 5820
Win32 bugfix update.   MetaPRL should now compile correctly on win32.
Also, the proxyedit application compiles with SSL.

Question: to use MetaPRL on win32 from a remote server, all you need
is the proxyedit application (if you want it).  Should we put it on
some standard site like www.metaprl.org?  Or should we commit it as
part of MetaPRL CVS.  The advantage of the latter is that we can
use MetaPRL even without global Internet access.


Revision 5820 - (view) (download) (annotate) - [select for diffs]
Modified Fri May 28 02:00:18 2004 UTC (17 years ago) by jyh
File length: 43719 byte(s)
Diff to previous 5755
This is the browser update I've been putting off.
   1. Browser now support both Mozilla *and* IE.
      I haven't tested on others like Safari.
      To get this to work, I had to use iframes
      and code custom menus.  Bleh.
   2. Connections are now SSL.  That is, you need to
      use https: connections instead of http:
   3. File editing is partially supported.  By default
      you edit in the browser.  However, you can define
      the application/x-metaprl MIME type to invoke
      an external editor.

      This is the main reason for using SSL.  At some
      point, we should do a code review to make sure
      we believe the security model
      (MD5 challenge/response).

TODO:
   1. Currently, edited files are not saved.  This is
      just a precaution for the moment.
   2. Need to add make/restart commands.  Easy, just
      haven't done it yet.

NOTE: I haven't checked that win32 compiles.  Working on that
next.


Revision 5755 - (view) (download) (annotate) - [select for diffs]
Modified Wed May 5 03:14:55 2004 UTC (17 years, 1 month ago) by jyh
File length: 38067 byte(s)
Diff to previous 5754
o Added term "handles" in browser mode.  These allow more precise
  term selections.
o "src" mode is parsable in most cases, at least in MMC.


Revision 5754 - (view) (download) (annotate) - [select for diffs]
Modified Tue May 4 21:36:46 2004 UTC (17 years, 1 month ago) by jyh
File length: 38017 byte(s)
Diff to previous 5736
Add a "View" window to control what is displayed in the browser.


Revision 5736 - (view) (download) (annotate) - [select for diffs]
Modified Wed Apr 28 04:30:09 2004 UTC (17 years, 1 month ago) by jyh
File length: 37694 byte(s)
Diff to previous 5732
This adds the final major feature I wanted to add to the browser:
copy/paste of terms into the rulebox.  There are two parts:
   1. The display form engine saves the terms in "slot" position
      into a table based on a string ID.
   2. Javascript to paste a term identified by ID into the rulebox.
To use this, just click on a term, and it will be pasted into the
rulebox.

The term in the rulebox is pasted in "src" mode.  Currently, terms
in "src" mode are not parsable by Term_grammar.  Ugh.

At long last, I declare the the browser interface to be in bugfix mode.

Bugfix TODO:
   1. Terms in "src" mode cannot be parsed.  Working on this.
      See Bugzilla bug #212.
   2. Need to add an "options" menu for things like:
      a. default "ls" flags
      b. handles on terms, so any term can be selected
   3. Remove the "Edit" menu, at least for now
   4. The mouse events are hardcoded in Lm_rformat_html.  Try to
      figure out a better way.


Revision 5732 - (view) (download) (annotate) - [select for diffs]
Modified Tue Apr 27 21:04:27 2004 UTC (17 years, 1 month ago) by jyh
File length: 35963 byte(s)
Diff to previous 5728
Added some more buttons to the browser interface.


Revision 5728 - (view) (download) (annotate) - [select for diffs]
Modified Mon Apr 26 18:07:02 2004 UTC (17 years, 1 month ago) by jyh
File length: 31243 byte(s)
Diff to previous 5704
A slight change to the browser interface.


Revision 5704 - (view) (download) (annotate) - [select for diffs]
Modified Fri Apr 23 21:30:22 2004 UTC (17 years, 2 months ago) by n8gray
File length: 31512 byte(s)
Diff to previous 5700
Browser command might be more than one word.  E.g. "open -a safari".


Revision 5700 - (view) (download) (annotate) - [select for diffs]
Modified Fri Apr 23 19:10:20 2004 UTC (17 years, 2 months ago) by jyh
File length: 31299 byte(s)
Diff to previous 5688
I had been working on the browser sporadically; here is a demo
update.

Changes:
   1. Use frames instead of div.  I'm still not sure what the
      advantage is beyond getting the scrollbars to work
      properly.  The control code is a lot more complicated
      of course.
   2. This history works with the arrow keys.
   3. Session support is better.

Tested just on Mozilla 1.4, I haven't tested on other browsers.

TODO:
   1. It is not possible to create a new session currently.
   2. Menubar should have some default non-context-sensitive
      entries.


Revision 5688 - (view) (download) (annotate) - [select for diffs]
Modified Wed Apr 21 15:54:55 2004 UTC (17 years, 2 months ago) by jyh
File length: 21769 byte(s)
Diff to previous 5680
Added some widgets to the browser.  Widgets are context-sensitive,
you can add them to the browser resource define in Browser_resource.

This version also demonstrates the use of iframes to display the
document.  I'm including for demo purposes, but I don't like it.

TODO:
   1. The upper menubar should always be present, even if
      the resource is not.
   2. The history should select the last entry.  It would be
      nice to catch arrow events in the input area, and scroll
      the history.


Revision 5680 - (view) (download) (annotate) - [select for diffs]
Modified Tue Apr 20 11:16:07 2004 UTC (17 years, 2 months ago) by nogin
File length: 19720 byte(s)
Diff to previous 5679
1. Make sure all session (i.e. non-special) URLs end with a /.
   Rationale:
      (a) It used to be the case that both ".../itt_fset" and ".../itt_fset/"
          would display the itt_fset theory. Obviously, the relative links
          would only work correctly in at most one of the two.
      (b) Between always stripping the last / and always insisting on the
          / ending I chose the latter since it makes figuring out the links
          much easier (e.g. this way the link to a rule in a theory listing
          does not have to include the theory name, just the rule name). Also,
          all the entries in MetaPRL are directory-like (since they are allowed
          to have subentries), so this appears to be consistent.

   As in a standard web server, attempt to go to a URL that does not end with
   a /, but is otherwise valid results in a redirect to a proper URL (i.e. with
   the missing / appended).

2. Linkified the rule and rewrite names. For now all of them are linkified, even
   the primitive ones - this should be fixed eventually. The CSS class is "rule_name".

3. Added the charset information (charset=utf-8) to all the html pages, as required
   in the standard.

4. Changed the style.css, page.html and style-related stuff in layout.js to be
   fully standards-complient (and pass the validator). Note that this also included
   deleting the non-standard "onResize" attribute. Unfortunalely, the divs still
   do not scroll.


Revision 5679 - (view) (download) (annotate) - [select for diffs]
Modified Tue Apr 20 09:07:38 2004 UTC (17 years, 2 months ago) by nogin
File length: 19287 byte(s)
Diff to previous 5678
- For Last-modified, do not forget to add 1900 to the year.

- Fixed the problem with accessing directories in /inputs. I got the backtrace
of this problem and it appears to be that open_in succeeds on directories and
only the input function (in Http_simple.copy) raises the Sys_error exception.
I ended up adding an explicit Unix.stat.


Revision 5678 - (view) (download) (annotate) - [select for diffs]
Modified Tue Apr 20 04:49:30 2004 UTC (17 years, 2 months ago) by jyh
File length: 19280 byte(s)
Diff to previous 5677
Some minor changes to the browser display mode.  This *should*
add:
   1. Catch chdir exceptions, so the browser doesn't abort
      if you give it a bad directory.
   2. The Short/Long mode is now handled in your browser,
      in Javascript.  If you refresh, you get short mode.
   3. Sessions.  This really only makes sense with threads,
      so you will normally use session/2.
   4. Use <span> instead of <font>.


Revision 5677 - (view) (download) (annotate) - [select for diffs]
Modified Tue Apr 20 04:09:03 2004 UTC (17 years, 2 months ago) by nogin
File length: 17840 byte(s)
Diff to previous 5674
When a non-existing theory is specified in a URL, print a Not_found error page,
instead of dying with an uncaught exception.


Revision 5674 - (view) (download) (annotate) - [select for diffs]
Modified Mon Apr 19 22:16:39 2004 UTC (17 years, 2 months ago) by nogin
File length: 17710 byte(s)
Diff to previous 5673
- Removed Lm_string_util.concal which was just duplicating String.concat.
- A bit more debugging in Shell_browser.


Revision 5673 - (view) (download) (annotate) - [select for diffs]
Modified Mon Apr 19 19:11:47 2004 UTC (17 years, 2 months ago) by jyh
File length: 17734 byte(s)
Diff to previous 5672
Browser layout should be updated using BODY.onLoad, not in the HEAD
section.  This now works with IT.  It also does active resizing when
then browser window is resized.


Revision 5672 - (view) (download) (annotate) - [select for diffs]
Modified Mon Apr 19 17:58:23 2004 UTC (17 years, 2 months ago) by jyh
File length: 17804 byte(s)
Diff to previous 5671
Use CSS stylesheets instead of hardcoding fonts and colors.


Revision 5671 - (view) (download) (annotate) - [select for diffs]
Modified Mon Apr 19 15:36:51 2004 UTC (17 years, 2 months ago) by jyh
File length: 17795 byte(s)
Diff to previous 5668
Display output correctly in browser mode.


Revision 5668 - (view) (download) (annotate) - [select for diffs]
Modified Mon Apr 19 01:46:53 2004 UTC (17 years, 2 months ago) by jyh
File length: 16615 byte(s)
Diff to previous 5666
This is an annoying commit.  It looks massive, but many of the changes
are just to "open" statements.  Here is the issue that is addressed.
   1. Format is a superset of Printf, and it is much better.
   2. MetaPRL's Rformat is a superset of Format, and it is much better.

This commit moves Rformat into libmojave, as Lm_rformat.  With this
commit, all output normally goes through Lm_rformat.  Feel free to
continue to use Format/Printf in special cases, but normal user output
should go through Lm_format/Lm_printf.  You will probably need to use
Lm_pervasives as well.

Lm_pervasives defines an (output_rbuffer : out_channel -> Lm_buffer.t -> unit)
that should be used instead of the print_text_channel function.

There is a new FORMAT option in mk/config.  Define FORMAT=Format to
enable old behavior if you have trouble.

There are two reasons behind this:
   1. We had a mix of files that use Printf and those that use Format
      for output.  This was a mess.  For instance format-style print
      directives (like "@[<hv 3>Content of text box@]@.") can't be
      used in raw Printf.  This meant that output functions had
      to be duplicated, one version for Printf, and one for Format.
      This commit solves the problem.
   2. Another reason, and the real reason behind this, is to allow
      output to be diverted based on the display device.


Revision 5666 - (view) (download) (annotate) - [select for diffs]
Modified Sat Apr 17 09:43:51 2004 UTC (17 years, 2 months ago) by nogin
File length: 16580 byte(s)
Diff to previous 5665
Removin unused/unneeded "open" statements.


Revision 5665 - (view) (download) (annotate) - [select for diffs]
Modified Sat Apr 17 04:00:48 2004 UTC (17 years, 2 months ago) by jyh
File length: 16613 byte(s)
Diff to previous 5661
Added message pane, but only toploop output is captured to the message window.
The next step is to divert exception output to the browser.


Revision 5661 - (view) (download) (annotate) - [select for diffs]
Modified Fri Apr 16 19:48:33 2004 UTC (17 years, 2 months ago) by jyh
File length: 16582 byte(s)
Diff to previous 5652
Trying to get output to display correctly in the browser.


Revision 5652 - (view) (download) (annotate) - [select for diffs]
Modified Thu Apr 15 05:49:33 2004 UTC (17 years, 2 months ago) by jyh
File length: 16062 byte(s)
Diff to previous 5651
Added support to start the browser at startup.  The typical use is

   setenv MP_BROWSER_COMMAND mozilla

This works with mozilla+Linux, but I'm not at all sure about
other combinations.


Revision 5651 - (view) (download) (annotate) - [select for diffs]
Modified Thu Apr 15 04:08:56 2004 UTC (17 years, 2 months ago) by jyh
File length: 14049 byte(s)
Diff to previous 5649
Added layout control based on browser window size (as Aleksey
suggested).  This info is not propagated to MetaPRL yet.

Added http service for raw files, with proper handling of
Last-Modified.


Revision 5649 - (view) (download) (annotate) - [select for diffs]
Modified Wed Apr 14 19:06:15 2004 UTC (17 years, 2 months ago) by jyh
File length: 13685 byte(s)
Diff to previous 5647
Removed support for frames.


Revision 5647 - (view) (download) (annotate) - [select for diffs]
Added Wed Apr 14 19:02:36 2004 UTC (17 years, 2 months ago) by jyh
File length: 15427 byte(s)
Added rudimentary support for display in a Web Browser.
To use, use the command "mpopt -browser [-port <int>]",
and follow the directions.  The interface is basically
the same as the normal toploop.  You type commands in
the input area, and MetaPRL displays the output.

Some notes about authentication.  The interface uses
challenge/response validation based on MD5 sums.
The connection requires a password, which is stored
in the clear in a protected file on the MetaPRL host,
and optionally as a cookie in your browser.  The
password is never sent in the clear over the network.

This isn't finished yet, but is pretty usable.  I would
appreciate comments.

TODO:
   1. Some exceptions are not being caught.  In general
      exception printing should be directed to the browser.
   2. Normal output should also be directed to the browser.
   3. Somehow Mozilla is not remembering cookies, which
      means that you have to enter your password more
      often than necessary.  Undoubtably this is due
      to my lack of Javascript knowledge.  If this can be
      fixed, the challenge can be updated frequently.
   4. There are some leftover files from a frame-based
      interface.  Frames are awkward, so I'll delete these
      files after the commit.
   5. I haven't tried it on Win32.


This form allows you to request diffs between any two revisions of this file. For each of the two "sides" of the diff, enter a numeric revision.

  Diffs between and
  Type of Diff should be a

  ViewVC Help
Powered by ViewVC 1.1.26