Skip to content
Success

Changes

Summary

  1. tuned: avoid ambiguity in scala3;
  2. clarified signature: avoid ambiguity in scala3;
  3. clarified signature: avoid ambiguity in scala3;
  4. more robust types (for scala3);
  5. tuned for scala3;
  6. proper indentation (relevant for scala3);
Changeset 75407:c7051638a38c by wenzelm:
tuned: avoid ambiguity in scala3;
The file was modified src/Pure/Thy/thy_header.scala (diff)
Changeset 75406:85e8b4c2b9a9 by wenzelm:
clarified signature: avoid ambiguity in scala3;
The file was modified src/Pure/General/json.scala (diff)
The file was modified src/Pure/PIDE/headless.scala (diff)
The file was modified src/Pure/PIDE/resources.scala (diff)
The file was modified src/Pure/Thy/sessions.scala (diff)
Changeset 75405:b13ab7d11b90 by wenzelm:
clarified signature: avoid ambiguity in scala3;
The file was modified src/Pure/General/json.scala (diff)
The file was modified src/Pure/Isar/parse.scala (diff)
The file was modified src/Pure/System/options.scala (diff)
The file was modified src/Pure/Thy/sessions.scala (diff)
The file was modified src/Pure/Thy/thy_element.scala (diff)
The file was modified src/Pure/Thy/thy_header.scala (diff)
The file was modified src/Pure/Tools/check_keywords.scala (diff)
Changeset 75404:a1363da718aa by wenzelm:
more robust types (for scala3);
The file was modified src/Tools/jEdit/src/query_dockable.scala (diff)
Changeset 75403:0f80086c000e by wenzelm:
tuned for scala3;
The file was modified src/Pure/General/json_api.scala (diff)
The file was modified src/Tools/Graphview/layout.scala (diff)
Changeset 75402:42fe20507496 by wenzelm:
proper indentation (relevant for scala3);
The file was modified src/Tools/jEdit/src/symbols_dockable.scala (diff)